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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  an12  550  cbval2  1893  cbvex2  1894  sbco2vh  1918  equsb3  1924  sbn  1925  sbim  1926  sbor  1927  sban  1928  sbco2h  1937  sbco2d  1939  sbco2vd  1940  sbcomv  1944  sbco3  1947  sbcom  1948  sbcom2v  1960  sbcom2v2  1961  sbcom2  1962  dfsb7  1966  sb7f  1967  sb7af  1968  sbal  1975  sbex  1979  sbco4lem  1981  moanim  2073  eq2tri  2199  eqsb3  2243  clelsb3  2244  clelsb4  2245  clelsb3f  2285  ralcom4  2708  rexcom4  2709  ceqsralt  2713  gencbvex  2732  gencbval  2734  ceqsrexbv  2816  euind  2871  reuind  2889  sbccomlem  2983  sbccom  2984  raaan  3469  elxp2  4557  eqbrriv  4634  dm0rn0  4756  dfres2  4871  qfto  4928  xpm  4960  rninxp  4982  fununi  5191  dfoprab2  5818  dfer2  6430  euen1  6696  xpsnen  6715  xpassen  6724  enq0enq  7246  prnmaxl  7303  prnminu  7304  suplocexprlemell  7528
  Copyright terms: Public domain W3C validator