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

Theorem 3bitr3i 209
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 185 . 2  |-  ( ch  <->  ps )
4 3bitr3i.3 . 2  |-  ( ps  <->  th )
53, 4bitri 183 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  an12  529  cbval2  1845  cbvex2  1846  sbco2v  1870  equsb3  1874  sbn  1875  sbim  1876  sbor  1877  sban  1878  sbco2h  1887  sbco2d  1889  sbco2vd  1890  sbcomv  1894  sbco3  1897  sbcom  1898  sbcom2v  1910  sbcom2v2  1911  sbcom2  1912  dfsb7  1916  sb7f  1917  sb7af  1918  sbal  1925  sbex  1929  sbco4lem  1931  moanim  2023  eq2tri  2148  eqsb3  2192  clelsb3  2193  clelsb4  2194  clelsb3f  2233  ralcom4  2644  rexcom4  2645  ceqsralt  2649  gencbvex  2668  gencbval  2670  ceqsrexbv  2751  euind  2805  reuind  2823  sbccomlem  2916  sbccom  2917  raaan  3394  elxp2  4472  eqbrriv  4548  dm0rn0  4668  dfres2  4779  qfto  4836  xpm  4868  rninxp  4889  fununi  5097  dfoprab2  5712  dfer2  6309  euen1  6575  xpsnen  6593  xpassen  6602  enq0enq  7053  prnmaxl  7110  prnminu  7111
  Copyright terms: Public domain W3C validator