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  763  orass  767  or32  770  dcan  933  dn1dc  960  an6  1321  excxor  1378  trubifal  1416  truxortru  1419  truxorfal  1420  falxortru  1421  falxorfal  1422  alrot4  1484  excom13  1687  sborv  1888  3exdistr  1913  4exdistr  1914  eeeanv  1931  ee4anv  1932  ee8anv  1933  sb3an  1956  sb9  1977  sbnf2  1979  sbco4  2005  2exsb  2007  sb8eu  2037  sb8euh  2047  sbmo  2083  2eu4  2117  2eu7  2118  elsb1  2153  elsb2  2154  r19.26-3  2605  rexcom13  2640  cbvreu  2699  ceqsex2  2775  ceqsex4v  2778  spc3gv  2828  ralrab2  2900  rexrab2  2902  reu2  2923  rmo4  2928  reu8  2931  rmo3f  2932  sbc3an  3022  rmo3  3052  dfss2  3142  ss2rab  3229  rabss  3230  ssrab  3231  dfdif3  3243  undi  3381  undif3ss  3394  difin2  3395  dfnul2  3422  disj  3469  disjsn  3651  snssb  3722  uni0c  3831  ssint  3856  iunss  3923  ssextss  4214  eqvinop  4237  opcom  4244  opeqsn  4246  opeqpr  4247  brabsb  4255  opelopabf  4268  opabm  4274  pofun  4306  sotritrieq  4319  uniuni  4445  ordsucim  4493  opeliunxp  4675  xpiundi  4678  brinxp2  4687  ssrel  4708  reliun  4741  cnvuni  4806  dmopab3  4833  opelres  4905  elres  4936  elsnres  4937  intirr  5007  ssrnres  5063  dminxp  5065  dfrel4v  5072  dmsnm  5086  rnco  5127  sb8iota  5177  dffun2  5218  dffun4f  5224  funco  5248  funcnveq  5271  fun11  5275  isarep1  5294  dff1o4  5461  dff1o6  5767  oprabid  5897  mpo2eqb  5974  ralrnmpo  5979  rexrnmpo  5980  opabex3d  6112  opabex3  6113  xporderlem  6222  f1od2  6226  tfr0dm  6313  tfrexlem  6325  frec0g  6388  nnaord  6500  ecid  6588  mptelixpg  6724  elixpsn  6725  mapsnen  6801  xpsnen  6811  xpcomco  6816  xpassen  6820  exmidontriimlem3  7212  nqnq0  7415  opelreal  7801  pitoregt0  7823  elnn0  9151  elxnn0  9214  elxr  9747  xrnepnf  9749  elfzuzb  9989  4fvwrd4  10110  elfzo2  10120  resqrexlemsqa  11001  fisumcom2  11414  modfsummod  11434  fprodcom2fi  11602  nnwosdc  12007  isprm2  12084  isprm4  12086  pythagtriplem2  12233  ntreq0  13203  txbas  13329  metrest  13577