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  764  orass  768  or32  771  dn1dc  962  an6  1332  excxor  1389  trubifal  1427  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  alrot4  1500  excom13  1703  sborv  1905  3exdistr  1930  4exdistr  1931  eeeanv  1952  ee4anv  1953  ee8anv  1954  sb3an  1977  sb9  1998  sbnf2  2000  sbco4  2026  2exsb  2028  sb8eu  2058  sb8euh  2068  sbmo  2104  2eu4  2138  2eu7  2139  elsb1  2174  elsb2  2175  r19.26-3  2627  rexcom13  2663  cbvreu  2727  ceqsex2  2804  ceqsex4v  2807  spc3gv  2857  ralrab2  2929  rexrab2  2931  reu2  2952  rmo4  2957  reu8  2960  rmo3f  2961  sbc3an  3051  rmo3  3081  dfss2  3172  ss2rab  3259  rabss  3260  ssrab  3261  dfdif3  3273  undi  3411  undif3ss  3424  difin2  3425  dfnul2  3452  disj  3499  disjsn  3684  snssb  3755  uni0c  3865  ssint  3890  iunss  3957  ssextss  4253  eqvinop  4276  opcom  4283  opeqsn  4285  opeqpr  4286  brabsb  4295  opelopabf  4309  opabm  4315  pofun  4347  sotritrieq  4360  uniuni  4486  ordsucim  4536  opeliunxp  4718  xpiundi  4721  brinxp2  4730  ssrel  4751  reliun  4784  cnvuni  4852  dmopab3  4879  opelres  4951  elres  4982  elsnres  4983  intirr  5056  ssrnres  5112  dminxp  5114  dfrel4v  5121  dmsnm  5135  rnco  5176  sb8iota  5226  dffun2  5268  dffun4f  5274  funco  5298  funcnveq  5321  fun11  5325  isarep1  5344  dff1o4  5512  dff1o6  5823  oprabid  5954  mpo2eqb  6032  ralrnmpo  6037  rexrnmpo  6038  opabex3d  6178  opabex3  6179  xporderlem  6289  f1od2  6293  tfr0dm  6380  tfrexlem  6392  frec0g  6455  nnaord  6567  ecid  6657  mptelixpg  6793  elixpsn  6794  mapsnen  6870  xpsnen  6880  xpcomco  6885  xpassen  6889  exmidontriimlem3  7290  nqnq0  7508  opelreal  7894  pitoregt0  7916  elnn0  9251  elxnn0  9314  elxr  9851  xrnepnf  9853  elfzuzb  10094  4fvwrd4  10215  elfzo2  10225  resqrexlemsqa  11189  fisumcom2  11603  modfsummod  11623  fprodcom2fi  11791  nnwosdc  12206  isprm2  12285  isprm4  12287  pythagtriplem2  12435  4sqlem12  12571  isnsg2  13333  isnsg4  13342  dfrhm2  13710  cnfldui  14145  ntreq0  14368  txbas  14494  metrest  14742  2lgslem4  15344