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

Theorem bitr2i 178
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr2i.1  |-  ( ph  <->  ps )
bitr2i.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
bitr2i  |-  ( ch  <->  ph )

Proof of Theorem bitr2i
StepHypRef Expression
1 bitr2i.1 . . 3  |-  ( ph  <->  ps )
2 bitr2i.2 . . 3  |-  ( ps  <->  ch )
31, 2bitri 177 . 2  |-  ( ph  <->  ch )
43bicomi 127 1  |-  ( ch  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3bitrri  200  3bitr2ri  202  3bitr4ri  206  nan  636  pm4.15  800  3or6  1229  sbal1yz  1893  2exsb  1901  moanim  1990  2eu4  2009  cvjust  2051  abbi  2167  sbc8g  2794  ss2rab  3044  unass  3128  unss  3145  undi  3213  difindiss  3219  disj  3296  unopab  3864  eqvinop  4008  pwexb  4234  dmun  4570  reldm0  4581  dmres  4660  imadmrn  4706  ssrnres  4791  dmsnm  4814  coundi  4850  coundir  4851  cnvpom  4888  xpcom  4892  fun11  4994  fununi  4995  funcnvuni  4996  isarep1  5013  fsn  5363  fconstfvm  5407  eufnfv  5417  acexmidlem2  5537  eloprabga  5619  funoprabg  5628  ralrnmpt2  5643  rexrnmpt2  5644  oprabrexex2  5785  dfer2  6138  euen1b  6314  xpsnen  6326  rexuz3  9817
  Copyright terms: Public domain W3C validator