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

Theorem bitr2i 184
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 183 . 2  |-  ( ph  <->  ch )
43bicomi 131 1  |-  ( ch  <->  ph )
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:  3bitrri  206  3bitr2ri  208  3bitr4ri  212  nan  687  pm4.15  689  3or6  1318  sbal1yz  1994  2exsb  2002  moanim  2093  2eu4  2112  cvjust  2165  abbi  2284  sbc8g  2962  ss2rab  3223  unass  3284  unss  3301  undi  3375  difindiss  3381  notm0  3435  disj  3463  unopab  4068  eqvinop  4228  pwexb  4459  dmun  4818  reldm0  4829  dmres  4912  imadmrn  4963  ssrnres  5053  dmsnm  5076  coundi  5112  coundir  5113  cnvpom  5153  xpcom  5157  fun11  5265  fununi  5266  funcnvuni  5267  isarep1  5284  fsn  5668  fconstfvm  5714  eufnfv  5726  acexmidlem2  5850  eloprabga  5940  funoprabg  5952  ralrnmpo  5967  rexrnmpo  5968  oprabrexex2  6109  dfer2  6514  euen1b  6781  xpsnen  6799  rexuz3  10954  tgval2  12845  ssntr  12916  metrest  13300  sinhalfpilem  13506
  Copyright terms: Public domain W3C validator