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  ssalel  3172  ss2rab  3260  rabss  3261  ssrab  3262  dfdif3  3274  undi  3412  undif3ss  3425  difin2  3426  dfnul2  3453  disj  3500  disjsn  3685  snssb  3756  uni0c  3866  ssint  3891  iunss  3958  ssextss  4254  eqvinop  4277  opcom  4284  opeqsn  4286  opeqpr  4287  brabsb  4296  opelopabf  4310  opabm  4316  pofun  4348  sotritrieq  4361  uniuni  4487  ordsucim  4537  opeliunxp  4719  xpiundi  4722  brinxp2  4731  ssrel  4752  reliun  4785  cnvuni  4853  dmopab3  4880  opelres  4952  elres  4983  elsnres  4984  intirr  5057  ssrnres  5113  dminxp  5115  dfrel4v  5122  dmsnm  5136  rnco  5177  sb8iota  5227  dffun2  5269  dffun4f  5275  funco  5299  funcnveq  5322  fun11  5326  isarep1  5345  dff1o4  5515  dff1o6  5826  oprabid  5957  mpo2eqb  6036  ralrnmpo  6041  rexrnmpo  6042  opabex3d  6187  opabex3  6188  xporderlem  6298  f1od2  6302  tfr0dm  6389  tfrexlem  6401  frec0g  6464  nnaord  6576  ecid  6666  mptelixpg  6802  elixpsn  6803  mapsnen  6879  xpsnen  6889  xpcomco  6894  xpassen  6898  exmidontriimlem3  7306  nqnq0  7525  opelreal  7911  pitoregt0  7933  elnn0  9268  elxnn0  9331  elxr  9868  xrnepnf  9870  elfzuzb  10111  4fvwrd4  10232  elfzo2  10242  resqrexlemsqa  11206  fisumcom2  11620  modfsummod  11640  fprodcom2fi  11808  nnwosdc  12231  isprm2  12310  isprm4  12312  pythagtriplem2  12460  4sqlem12  12596  isnsg2  13409  isnsg4  13418  dfrhm2  13786  cnfldui  14221  ntreq0  14452  txbas  14578  metrest  14826  2lgslem4  15428