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

Theorem bitr2i 185
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 184 . 2  |-  ( ph  <->  ch )
43bicomi 132 1  |-  ( ch  <->  ph )
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:  3bitrri  207  3bitr2ri  209  3bitr4ri  213  nan  692  pm4.15  694  3or6  1323  sbal1yz  2001  2exsb  2009  moanim  2100  2eu4  2119  cvjust  2172  abbi  2291  sbc8g  2970  ss2rab  3231  unass  3292  unss  3309  undi  3383  difindiss  3389  notm0  3443  disj  3471  unopab  4079  eqvinop  4240  pwexb  4471  dmun  4830  reldm0  4841  dmres  4924  imadmrn  4976  ssrnres  5067  dmsnm  5090  coundi  5126  coundir  5127  cnvpom  5167  xpcom  5171  fun11  5279  fununi  5280  funcnvuni  5281  isarep1  5298  fsn  5684  fconstfvm  5730  eufnfv  5742  acexmidlem2  5866  eloprabga  5956  funoprabg  5968  ralrnmpo  5983  rexrnmpo  5984  oprabrexex2  6125  dfer2  6530  euen1b  6797  xpsnen  6815  rexuz3  10983  tgval2  13218  ssntr  13289  metrest  13673  sinhalfpilem  13879
  Copyright terms: Public domain W3C validator