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  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  3572  disjsn  3767  snssb  3843  uni0c  3956  ssint  3981  iunss  4048  ssextss  4355  eqvinop  4378  opcom  4386  opeqsn  4388  opeqpr  4389  brabsb  4398  opelopabf  4412  opabm  4418  pofun  4452  sotritrieq  4465  uniuni  4592  ordsucim  4642  opeliunxp  4825  xpiundi  4828  brinxp2  4837  ssrel  4858  reliun  4893  cnvuni  4961  dmopab3  4989  opelres  5063  elres  5094  elsnres  5095  intirr  5169  ssrnres  5225  dminxp  5227  dfrel4v  5234  dmsnm  5248  rnco  5289  sb8iota  5340  dffun2  5382  dffun4f  5388  funco  5412  funcnveq  5439  fun11  5443  isarep1  5462  dff1o4  5642  dff1o6  5972  oprabid  6107  mpo2eqb  6188  ralrnmpo  6193  rexrnmpo  6194  opabex3d  6340  opabex3  6341  xporderlem  6457  f1od2  6461  tfr0dm  6583  tfrexlem  6595  frec0g  6658  nnaord  6772  ecid  6862  mptelixpg  7006  elixpsn  7007  mapsnen  7090  xpsnen  7109  xpcomco  7114  xpassen  7118  exmidontriimlem3  7569  nqnq0  7798  opelreal  8184  pitoregt0  8206  elnn0  9544  elxnn0  9611  elxr  10157  xrnepnf  10159  elfzuzb  10401  4fvwrd4  10525  elfzo2  10535  swrdnd  11409  resqrexlemsqa  11768  fisumcom2  12183  modfsummod  12203  fprodcom2fi  12371  nnwosdc  12794  isprm2  12873  isprm4  12875  pythagtriplem2  13023  4sqlem12  13159  isnsg2  13983  isnsg4  13992  dfrhm2  14434  cnfldui  14896  ntreq0  15156  txbas  15282  metrest  15530  2lgslem4  16136  umgr2edg1  16364  isclwwlk  16549  isclwwlknx  16571  clwwlkn1  16573  clwwlkn2  16576  clwwlknonel  16587  iseupthf1o  16603