Theorem 3bitri 205

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 183	. 2 |- ( ps <-> th )
5	1, 4	bitri 183	1 |- ( ph <-> th )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1i  227  an32  557  orbi1i  758  orass  762  or32  765  dcan  928  dn1dc  955  an6  1316  excxor  1373  trubifal  1411  truxortru  1414  truxorfal  1415  falxortru  1416  falxorfal  1417  alrot4  1479  excom13  1682  sborv  1883  3exdistr  1908  4exdistr  1909  eeeanv  1926  ee4anv  1927  ee8anv  1928  sb3an  1951  sb9  1972  sbnf2  1974  sbco4  2000  2exsb  2002  sb8eu  2032  sb8euh  2042  sbmo  2078  2eu4  2112  2eu7  2113  elsb1  2148  elsb2  2149  r19.26-3  2600  rexcom13  2635  cbvreu  2694  ceqsex2  2770  ceqsex4v  2773  spc3gv  2823  ralrab2  2895  rexrab2  2897  reu2  2918  rmo4  2923  reu8  2926  rmo3f  2927  sbc3an  3016  rmo3  3046  dfss2  3136  ss2rab  3223  rabss  3224  ssrab  3225  dfdif3  3237  undi  3375  undif3ss  3388  difin2  3389  dfnul2  3416  disj  3463  disjsn  3645  uni0c  3822  ssint  3847  iunss  3914  ssextss  4205  eqvinop  4228  opcom  4235  opeqsn  4237  opeqpr  4238  brabsb  4246  opelopabf  4259  opabm  4265  pofun  4297  sotritrieq  4310  uniuni  4436  ordsucim  4484  opeliunxp  4666  xpiundi  4669  brinxp2  4678  ssrel  4699  reliun  4732  cnvuni  4797  dmopab3  4824  opelres  4896  elres  4927  elsnres  4928  intirr  4997  ssrnres  5053  dminxp  5055  dfrel4v  5062  dmsnm  5076  rnco  5117  sb8iota  5167  dffun2  5208  dffun4f  5214  funco  5238  funcnveq  5261  fun11  5265  isarep1  5284  dff1o4  5450  dff1o6  5755  oprabid  5885  mpo2eqb  5962  ralrnmpo  5967  rexrnmpo  5968  opabex3d  6100  opabex3  6101  xporderlem  6210  f1od2  6214  tfr0dm  6301  tfrexlem  6313  frec0g  6376  nnaord  6488  ecid  6576  mptelixpg  6712  elixpsn  6713  mapsnen  6789  xpsnen  6799  xpcomco  6804  xpassen  6808  exmidontriimlem3  7200  nqnq0  7403  opelreal  7789  pitoregt0  7811  elnn0  9137  elxnn0  9200  elxr  9733  xrnepnf  9735  elfzuzb  9975  4fvwrd4  10096  elfzo2  10106  resqrexlemsqa  10988  fisumcom2  11401  modfsummod  11421  fprodcom2fi  11589  nnwosdc  11994  isprm2  12071  isprm4  12073  pythagtriplem2  12220  ntreq0  12926  txbas  13052  metrest  13300