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  564  orbi1i  771  orass  775  or32  778  dn1dc  969  an6  1358  excxor  1423  trubifal  1461  truxortru  1464  truxorfal  1465  falxortru  1466  falxorfal  1467  alrot4  1535  excom13  1737  sborv  1941  3exdistr  1967  4exdistr  1968  eeeanv  1989  ee4anv  1990  ee8anv  1991  sb3an  2014  sb9  2035  sbnf2  2037  sbco4  2063  2exsb  2065  sb8eu  2095  sb8euh  2105  sbmo  2142  2eu4  2176  2eu7  2177  elsb1  2212  elsb2  2213  r19.26-3  2675  rexcom13  2711  cbvreu  2778  ceqsex2  2857  ceqsex4v  2860  spc3gv  2912  ralrab2  2984  rexrab2  2986  reu2  3007  rmo4  3012  reu8  3015  rmo3f  3016  sbc3an  3106  reu8nf  3126  rmo3  3137  ssalel  3228  ss2rab  3316  rabss  3317  ssrab  3318  dfdif3  3331  undi  3471  undif3ss  3484  difin2  3485  dfnul2  3512  disj  3559  disjsn  3753  snssb  3829  uni0c  3942  ssint  3967  iunss  4034  ssextss  4338  eqvinop  4361  opcom  4369  opeqsn  4371  opeqpr  4372  brabsb  4381  opelopabf  4395  opabm  4401  pofun  4435  sotritrieq  4448  uniuni  4574  ordsucim  4624  opeliunxp  4807  xpiundi  4810  brinxp2  4819  ssrel  4840  reliun  4875  cnvuni  4943  dmopab3  4971  opelres  5045  elres  5076  elsnres  5077  intirr  5151  ssrnres  5207  dminxp  5209  dfrel4v  5216  dmsnm  5230  rnco  5271  sb8iota  5322  dffun2  5364  dffun4f  5370  funco  5394  funcnveq  5421  fun11  5425  isarep1  5444  dff1o4  5624  dff1o6  5951  oprabid  6084  mpo2eqb  6165  ralrnmpo  6170  rexrnmpo  6171  opabex3d  6316  opabex3  6317  xporderlem  6429  f1od2  6433  tfr0dm  6555  tfrexlem  6567  frec0g  6630  nnaord  6744  ecid  6834  mptelixpg  6971  elixpsn  6972  mapsnen  7055  xpsnen  7074  xpcomco  7079  xpassen  7083  exmidontriimlem3  7532  nqnq0  7758  opelreal  8144  pitoregt0  8166  elnn0  9500  elxnn0  9567  elxr  10112  xrnepnf  10114  elfzuzb  10356  4fvwrd4  10478  elfzo2  10488  swrdnd  11355  resqrexlemsqa  11713  fisumcom2  12128  modfsummod  12148  fprodcom2fi  12316  nnwosdc  12739  isprm2  12818  isprm4  12820  pythagtriplem2  12968  4sqlem12  13104  isnsg2  13937  isnsg4  13946  dfrhm2  14316  cnfldui  14754  ntreq0  15014  txbas  15140  metrest  15388  2lgslem4  15993  umgr2edg1  16221  isclwwlk  16406  isclwwlknx  16428  clwwlkn1  16430  clwwlkn2  16433  clwwlknonel  16444  iseupthf1o  16460