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

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

Proof of Theorem bitr3i
StepHypRef Expression
1 bitr3i.1 . . 3  |-  ( ps  <->  ph )
21bicomi 132 . 2  |-  ( ph  <->  ps )
3 bitr3i.2 . 2  |-  ( ps  <->  ch )
42, 3bitri 184 1  |-  ( ph  <->  ch )
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  3bitr3i  210  3bitr3ri  211  anandi  590  anandir  591  xchnxbi  680  orordi  773  orordir  774  sbco3v  1969  sbco4  2007  elsb1  2155  elsb2  2156  abeq1i  2289  cbvabw  2300  r19.41  2632  rexcom4a  2761  moeq  2912  mosubt  2914  2reuswapdc  2941  nfcdeq  2959  sbcid  2978  sbcco2  2985  sbc7  2989  sbcie2g  2996  eqsbc1  3002  sbcralt  3039  sbcrext  3040  cbvralcsf  3119  cbvrexcsf  3120  cbvrabcsf  3122  abss  3224  ssab  3225  difrab  3409  abn0m  3448  prsspw  3763  disjnim  3991  brab1  4047  unopab  4079  exss  4223  uniuni  4447  elvvv  4685  eliunxp  4761  ralxp  4765  rexxp  4766  opelco  4794  reldm0  4840  resieq  4912  resiexg  4947  iss  4948  imai  4979  cnvsym  5007  intasym  5008  asymref  5009  codir  5012  poirr2  5016  rninxp  5067  cnvsom  5167  funopg  5245  fin  5397  f1cnvcnv  5427  fndmin  5618  resoprab  5964  mpo2eqb  5977  ov6g  6005  offval  6083  dfopab2  6183  dfoprab3s  6184  fmpox  6194  spc2ed  6227  brtpos0  6246  dftpos3  6256  tpostpos  6258  ercnv  6549  xpcomco  6819  xpassen  6823  phpm  6858  ctssdccl  7103  elni2  7291  elfz2nn0  10085  elfzmlbp  10105  clim0  11264  nnwosdc  12010  isstructim  12446  srgrmhm  12990  ntreq0  13265  cnmptcom  13431  dedekindicclemicc  13743
  Copyright terms: Public domain W3C validator