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 )

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:  bibi1i  228  an32  562  orbi1i  764  orass  768  or32  771  dn1dc  962  an6  1332  excxor  1389  trubifal  1427  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  alrot4  1497  excom13  1700  sborv  1902  3exdistr  1927  4exdistr  1928  eeeanv  1949  ee4anv  1950  ee8anv  1951  sb3an  1974  sb9  1995  sbnf2  1997  sbco4  2023  2exsb  2025  sb8eu  2055  sb8euh  2065  sbmo  2101  2eu4  2135  2eu7  2136  elsb1  2171  elsb2  2172  r19.26-3  2624  rexcom13  2660  cbvreu  2724  ceqsex2  2801  ceqsex4v  2804  spc3gv  2854  ralrab2  2926  rexrab2  2928  reu2  2949  rmo4  2954  reu8  2957  rmo3f  2958  sbc3an  3048  rmo3  3078  dfss2  3169  ss2rab  3256  rabss  3257  ssrab  3258  dfdif3  3270  undi  3408  undif3ss  3421  difin2  3422  dfnul2  3449  disj  3496  disjsn  3681  snssb  3752  uni0c  3862  ssint  3887  iunss  3954  ssextss  4250  eqvinop  4273  opcom  4280  opeqsn  4282  opeqpr  4283  brabsb  4292  opelopabf  4306  opabm  4312  pofun  4344  sotritrieq  4357  uniuni  4483  ordsucim  4533  opeliunxp  4715  xpiundi  4718  brinxp2  4727  ssrel  4748  reliun  4781  cnvuni  4849  dmopab3  4876  opelres  4948  elres  4979  elsnres  4980  intirr  5053  ssrnres  5109  dminxp  5111  dfrel4v  5118  dmsnm  5132  rnco  5173  sb8iota  5223  dffun2  5265  dffun4f  5271  funco  5295  funcnveq  5318  fun11  5322  isarep1  5341  dff1o4  5509  dff1o6  5820  oprabid  5951  mpo2eqb  6029  ralrnmpo  6034  rexrnmpo  6035  opabex3d  6175  opabex3  6176  xporderlem  6286  f1od2  6290  tfr0dm  6377  tfrexlem  6389  frec0g  6452  nnaord  6564  ecid  6654  mptelixpg  6790  elixpsn  6791  mapsnen  6867  xpsnen  6877  xpcomco  6882  xpassen  6886  exmidontriimlem3  7285  nqnq0  7503  opelreal  7889  pitoregt0  7911  elnn0  9245  elxnn0  9308  elxr  9845  xrnepnf  9847  elfzuzb  10088  4fvwrd4  10209  elfzo2  10219  resqrexlemsqa  11171  fisumcom2  11584  modfsummod  11604  fprodcom2fi  11772  nnwosdc  12179  isprm2  12258  isprm4  12260  pythagtriplem2  12407  4sqlem12  12543  isnsg2  13276  isnsg4  13285  dfrhm2  13653  cnfldui  14088  ntreq0  14311  txbas  14437  metrest  14685  2lgslem4  15260