ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr3i Unicode version

Theorem 3bitr3i 210
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
Hypotheses
Ref Expression
3bitr3i.1  |-  ( ph  <->  ps )
3bitr3i.2  |-  ( ph  <->  ch )
3bitr3i.3  |-  ( ps  <->  th )
Assertion
Ref Expression
3bitr3i  |-  ( ch  <->  th )

Proof of Theorem 3bitr3i
StepHypRef Expression
1 3bitr3i.2 . . 3  |-  ( ph  <->  ch )
2 3bitr3i.1 . . 3  |-  ( ph  <->  ps )
31, 2bitr3i 186 . 2  |-  ( ch  <->  ps )
4 3bitr3i.3 . 2  |-  ( ps  <->  th )
53, 4bitri 184 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  an12  561  cbval2  1921  cbvex2  1922  sbco2vh  1945  equsb3  1951  sbn  1952  sbim  1953  sbor  1954  sban  1955  sbco2h  1964  sbco2d  1966  sbco2vd  1967  sbcomv  1971  sbco3  1974  sbcom  1975  sbcom2v  1985  sbcom2v2  1986  sbcom2  1987  dfsb7  1991  sb7f  1992  sb7af  1993  sbal  2000  sbex  2004  sbco4lem  2006  moanim  2100  eq2tri  2237  eqsb1  2281  clelsb1  2282  clelsb2  2283  clelsb1f  2323  ralcom4  2760  rexcom4  2761  ceqsralt  2765  gencbvex  2784  gencbval  2786  ceqsrexbv  2869  euind  2925  reuind  2943  sbccomlem  3038  sbccom  3039  raaan  3530  elxp2  4645  eqbrriv  4722  dm0rn0  4845  dfres2  4960  qfto  5019  xpm  5051  rninxp  5073  fununi  5285  dfoprab2  5922  dfer2  6536  euen1  6802  xpsnen  6821  xpassen  6830  enq0enq  7430  prnmaxl  7487  prnminu  7488  suplocexprlemell  7712
  Copyright terms: Public domain W3C validator