doc-src/Ref/thm.tex
 changeset 3524 c02cb15830de parent 3485 f27a30a18a17 child 3657 48b8efdd1b80
equal inserted replaced
3523:23eae933c2d9 3524:c02cb15830de
   354 $\infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad  354 \[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad  355 \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi}$
   355    \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi}  \]
   356
   356
   357 \index{meta-equality}
   357 \index{meta-equality}
   358 Equality of truth values means logical equivalence:
   358 Equality of truth values means logical equivalence:
   359 $\infer[({\equiv}I)]{\phi\equiv\psi}{\infer*{\psi}{[\phi]} &  359 \[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi &  360 \infer*{\phi}{[\psi]}}   360 \psi\Imp\phi}  361 \qquad  361 \qquad  362 \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi}$
   362    \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi}   \]
   363
   363
   364 The {\bf equality} rules are reflexivity, symmetry, and transitivity:
   364 The {\bf equality} rules are reflexivity, symmetry, and transitivity:
   365 \[ {a\equiv a}\,(refl)  \qquad
   365 \[ {a\equiv a}\,(refl)  \qquad