Theorem 3bitri 206

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

Step	Hyp	Ref	Expression
1		3bitri.1	. 2 |- ( ph <-> ps )
2		3bitri.2	. . 3 |- ( ps <-> ch )
3		3bitri.3	. . 3 |- ( ch <-> th )
4	2, 3	bitri 184	. 2 |- ( ps <-> th )
5	1, 4	bitri 184	1 |- ( ph <-> th )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bibi1i  228  an32  568  orbi1i  775  orass  779  or32  782  dn1dc  973  an6  1362  excxor  1427  trubifal  1465  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  alrot4  1539  excom13  1741  sborv  1945  3exdistr  1971  4exdistr  1972  eeeanv  1993  ee4anv  1994  ee8anv  1995  sb3an  2018  sb9  2039  sbnf2  2041  sbco4  2067  2exsb  2069  sb8eu  2099  sb8euh  2109  sbmo  2146  2eu4  2180  2eu7  2181  elsb1  2216  elsb2  2217  r19.26-3  2681  rexcom13  2717  cbvreu  2784  ceqsex2  2863  ceqsex4v  2866  spc3gv  2918  ralrab2  2991  rexrab2  2993  reu2  3014  rmo4  3019  reu8  3022  rmo3f  3023  sbc3an  3113  reu8nf  3133  rmo3  3144  ssalel  3235  ss2rab  3324  rabss  3325  ssrab  3326  dfdif3  3339  undi  3479  undif3ss  3492  difin2  3493  disj  3573  disjsn  3771  snssb  3848  uni0c  3961  ssint  3986  iunss  4053  ssextss  4360  eqvinop  4383  opcom  4391  opeqsn  4393  opeqpr  4394  brabsb  4403  opelopabf  4417  opabm  4423  pofun  4457  sotritrieq  4470  uniuni  4597  ordsucim  4647  opeliunxp  4830  xpiundi  4833  brinxp2  4842  ssrel  4863  reliun  4898  cnvuni  4966  dmopab3  4994  opelres  5068  elres  5099  elsnres  5100  intirr  5174  ssrnres  5230  dminxp  5232  dfrel4v  5239  dmsnm  5253  rnco  5294  sb8iota  5345  dffun2  5387  dffun4f  5393  funco  5417  funcnveq  5444  fun11  5448  isarep1  5467  dff1o4  5647  dff1o6  5982  oprabid  6117  mpo2eqb  6198  ralrnmpo  6203  rexrnmpo  6204  opabex3d  6350  opabex3  6351  xporderlem  6467  f1od2  6471  tfr0dm  6593  tfrexlem  6605  frec0g  6668  nnaord  6782  ecid  6872  mptelixpg  7016  elixpsn  7017  mapsnen  7100  xpsnen  7119  xpcomco  7124  xpassen  7128  exmidontriimlem3  7579  nqnq0  7808  opelreal  8194  pitoregt0  8216  elnn0  9569  elxnn0  9636  elxr  10188  xrnepnf  10190  elfzuzb  10432  4fvwrd4  10557  elfzo2  10567  swrdnd  11445  resqrexlemsqa  11804  fisumcom2  12221  modfsummod  12241  fprodcom2fi  12409  nnwosdc  12832  isprm2  12911  isprm4  12913  pythagtriplem2  13065  4sqlem12  13201  isnsg2  14055  isnsg4  14064  dfrhm2  14510  cnfldui  14973  isassa  15051  ntreq0  15282  txbas  15408  metrest  15656  2lgslem4  16320  umgr2edg1  16548  isclwwlk  16733  isclwwlknx  16755  clwwlkn1  16757  clwwlkn2  16760  clwwlknonel  16771  iseupthf1o  16787  alsanmo  17249  ralsanmo  17250