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  552  orbi1i  753  orass  757  or32  760  dcan  923  dn1dc  950  an6  1311  excxor  1368  trubifal  1406  truxortru  1409  truxorfal  1410  falxortru  1411  falxorfal  1412  alrot4  1474  excom13  1677  sborv  1878  3exdistr  1903  4exdistr  1904  eeeanv  1921  ee4anv  1922  ee8anv  1923  sb3an  1946  sb9  1967  sbnf2  1969  sbco4  1995  2exsb  1997  sb8eu  2027  sb8euh  2037  sbmo  2073  2eu4  2107  2eu7  2108  elsb1  2143  elsb2  2144  r19.26-3  2596  rexcom13  2631  cbvreu  2690  ceqsex2  2766  ceqsex4v  2769  spc3gv  2819  ralrab2  2891  rexrab2  2893  reu2  2914  rmo4  2919  reu8  2922  rmo3f  2923  sbc3an  3012  rmo3  3042  dfss2  3131  ss2rab  3218  rabss  3219  ssrab  3220  dfdif3  3232  undi  3370  undif3ss  3383  difin2  3384  dfnul2  3411  disj  3457  disjsn  3638  uni0c  3815  ssint  3840  iunss  3907  ssextss  4198  eqvinop  4221  opcom  4228  opeqsn  4230  opeqpr  4231  brabsb  4239  opelopabf  4252  opabm  4258  pofun  4290  sotritrieq  4303  uniuni  4429  ordsucim  4477  opeliunxp  4659  xpiundi  4662  brinxp2  4671  ssrel  4692  reliun  4725  cnvuni  4790  dmopab3  4817  opelres  4889  elres  4920  elsnres  4921  intirr  4990  ssrnres  5046  dminxp  5048  dfrel4v  5055  dmsnm  5069  rnco  5110  sb8iota  5160  dffun2  5198  dffun4f  5204  funco  5228  funcnveq  5251  fun11  5255  isarep1  5274  dff1o4  5440  dff1o6  5744  oprabid  5874  mpo2eqb  5951  ralrnmpo  5956  rexrnmpo  5957  opabex3d  6089  opabex3  6090  xporderlem  6199  f1od2  6203  tfr0dm  6290  tfrexlem  6302  frec0g  6365  nnaord  6477  ecid  6564  mptelixpg  6700  elixpsn  6701  mapsnen  6777  xpsnen  6787  xpcomco  6792  xpassen  6796  exmidontriimlem3  7179  nqnq0  7382  opelreal  7768  pitoregt0  7790  elnn0  9116  elxnn0  9179  elxr  9712  xrnepnf  9714  elfzuzb  9954  4fvwrd4  10075  elfzo2  10085  resqrexlemsqa  10966  fisumcom2  11379  modfsummod  11399  fprodcom2fi  11567  nnwosdc  11972  isprm2  12049  isprm4  12051  pythagtriplem2  12198  ntreq0  12772  txbas  12898  metrest  13146