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  768  orass  772  or32  775  dn1dc  966  an6  1355  excxor  1420  trubifal  1458  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  alrot4  1532  excom13  1735  sborv  1937  3exdistr  1962  4exdistr  1963  eeeanv  1984  ee4anv  1985  ee8anv  1986  sb3an  2009  sb9  2030  sbnf2  2032  sbco4  2058  2exsb  2060  sb8eu  2090  sb8euh  2100  sbmo  2137  2eu4  2171  2eu7  2172  elsb1  2207  elsb2  2208  r19.26-3  2661  rexcom13  2697  cbvreu  2763  ceqsex2  2841  ceqsex4v  2844  spc3gv  2896  ralrab2  2968  rexrab2  2970  reu2  2991  rmo4  2996  reu8  2999  rmo3f  3000  sbc3an  3090  reu8nf  3110  rmo3  3121  ssalel  3212  ss2rab  3300  rabss  3301  ssrab  3302  dfdif3  3314  undi  3452  undif3ss  3465  difin2  3466  dfnul2  3493  disj  3540  disjsn  3728  snssb  3800  uni0c  3913  ssint  3938  iunss  4005  ssextss  4305  eqvinop  4328  opcom  4336  opeqsn  4338  opeqpr  4339  brabsb  4348  opelopabf  4362  opabm  4368  pofun  4402  sotritrieq  4415  uniuni  4541  ordsucim  4591  opeliunxp  4773  xpiundi  4776  brinxp2  4785  ssrel  4806  reliun  4839  cnvuni  4907  dmopab3  4935  opelres  5009  elres  5040  elsnres  5041  intirr  5114  ssrnres  5170  dminxp  5172  dfrel4v  5179  dmsnm  5193  rnco  5234  sb8iota  5285  dffun2  5327  dffun4f  5333  funco  5357  funcnveq  5383  fun11  5387  isarep1  5406  dff1o4  5579  dff1o6  5899  oprabid  6032  mpo2eqb  6113  ralrnmpo  6118  rexrnmpo  6119  opabex3d  6264  opabex3  6265  xporderlem  6375  f1od2  6379  tfr0dm  6466  tfrexlem  6478  frec0g  6541  nnaord  6653  ecid  6743  mptelixpg  6879  elixpsn  6880  mapsnen  6962  xpsnen  6976  xpcomco  6981  xpassen  6985  exmidontriimlem3  7401  nqnq0  7624  opelreal  8010  pitoregt0  8032  elnn0  9367  elxnn0  9430  elxr  9968  xrnepnf  9970  elfzuzb  10211  4fvwrd4  10332  elfzo2  10342  swrdnd  11186  resqrexlemsqa  11530  fisumcom2  11944  modfsummod  11964  fprodcom2fi  12132  nnwosdc  12555  isprm2  12634  isprm4  12636  pythagtriplem2  12784  4sqlem12  12920  isnsg2  13735  isnsg4  13744  dfrhm2  14112  cnfldui  14547  ntreq0  14800  txbas  14926  metrest  15174  2lgslem4  15776  umgr2edg1  16001