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

Theorem 3bitri 199
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitri.1  |-  ( ph  <->  ps )
3bitri.2  |-  ( ps  <->  ch )
3bitri.3  |-  ( ch  <->  th )
Assertion
Ref Expression
3bitri  |-  ( ph  <->  th )

Proof of Theorem 3bitri
StepHypRef Expression
1 3bitri.1 . 2  |-  ( ph  <->  ps )
2 3bitri.2 . . 3  |-  ( ps  <->  ch )
3 3bitri.3 . . 3  |-  ( ch  <->  th )
42, 3bitri 177 . 2  |-  ( ps  <->  th )
51, 4bitri 177 1  |-  ( ph  <->  th )
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:  bibi1i  221  an32  504  orbi1i  690  orass  694  or32  697  dcan  853  dn1dc  878  an6  1227  excxor  1285  trubifal  1323  truxortru  1326  truxorfal  1327  falxortru  1328  falxorfal  1329  alrot4  1391  excom13  1595  sborv  1786  3exdistr  1808  4exdistr  1809  eeeanv  1824  ee4anv  1825  ee8anv  1826  sb3an  1848  elsb3  1868  elsb4  1869  sb9  1871  sbnf2  1873  sbco4  1899  2exsb  1901  sb8eu  1929  sb8euh  1939  sbmo  1975  2eu4  2009  2eu7  2010  r19.26-3  2460  rexcom13  2492  cbvreu  2548  ceqsex2  2611  ceqsex4v  2614  spc3gv  2662  ralrab2  2729  rexrab2  2731  reu2  2752  rmo4  2757  reu8  2760  sbc3an  2847  rmo3  2877  dfss2  2962  ss2rab  3044  rabss  3045  ssrab  3046  undi  3213  undif3ss  3226  difin2  3227  dfnul2  3254  disj  3296  disjsn  3460  uni0c  3634  ssint  3659  iunss  3726  ssextss  3984  eqvinop  4008  opcom  4015  opeqsn  4017  opeqpr  4018  brabsb  4026  opelopabf  4039  opabm  4045  pofun  4077  sotritrieq  4090  uniuni  4211  ordsucim  4254  opeliunxp  4423  xpiundi  4426  brinxp2  4435  ssrel  4456  reliun  4486  cnvuni  4549  dmopab3  4576  opelres  4645  elres  4674  elsnres  4675  intirr  4739  ssrnres  4791  dminxp  4793  dfrel4v  4800  dmsnm  4814  rnco  4855  sb8iota  4902  dffun2  4940  dffun4f  4946  funco  4968  funcnveq  4990  fun11  4994  isarep1  5013  dff1o4  5162  dff1o6  5444  oprabid  5565  mpt22eqb  5638  ralrnmpt2  5643  rexrnmpt2  5644  opabex3d  5776  opabex3  5777  xporderlem  5880  f1od2  5884  tfr0  5968  tfrexlem  5979  frec0g  6014  nnaord  6113  ecid  6200  xpsnen  6326  xpcomco  6331  xpassen  6335  nqnq0  6597  opelreal  6962  pitoregt0  6983  elnn0  8241  elxr  8797  xrnepnf  8801  elfzuzb  8986  4fvwrd4  9099  elfzo2  9109  resqrexlemsqa  9851
  Copyright terms: Public domain W3C validator