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-1 5  ax-2 6  ax-mp 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  532  orbi1i  721  orass  725  or32  728  dcan  886  dn1dc  912  an6  1267  excxor  1324  trubifal  1362  truxortru  1365  truxorfal  1366  falxortru  1367  falxorfal  1368  alrot4  1430  excom13  1635  sborv  1829  3exdistr  1852  4exdistr  1853  eeeanv  1868  ee4anv  1869  ee8anv  1870  sb3an  1892  elsb3  1912  elsb4  1913  sb9  1915  sbnf2  1917  sbco4  1943  2exsb  1945  sb8eu  1973  sb8euh  1983  sbmo  2019  2eu4  2053  2eu7  2054  r19.26-3  2521  rexcom13  2554  cbvreu  2610  ceqsex2  2681  ceqsex4v  2684  spc3gv  2733  ralrab2  2802  rexrab2  2804  reu2  2825  rmo4  2830  reu8  2833  rmo3f  2834  sbc3an  2922  rmo3  2952  dfss2  3036  ss2rab  3120  rabss  3121  ssrab  3122  dfdif3  3133  undi  3271  undif3ss  3284  difin2  3285  dfnul2  3312  disj  3358  disjsn  3532  uni0c  3709  ssint  3734  iunss  3801  ssextss  4080  eqvinop  4103  opcom  4110  opeqsn  4112  opeqpr  4113  brabsb  4121  opelopabf  4134  opabm  4140  pofun  4172  sotritrieq  4185  uniuni  4310  ordsucim  4354  opeliunxp  4532  xpiundi  4535  brinxp2  4544  ssrel  4565  reliun  4598  cnvuni  4663  dmopab3  4690  opelres  4760  elres  4791  elsnres  4792  intirr  4861  ssrnres  4917  dminxp  4919  dfrel4v  4926  dmsnm  4940  rnco  4981  sb8iota  5031  dffun2  5069  dffun4f  5075  funco  5099  funcnveq  5122  fun11  5126  isarep1  5145  dff1o4  5309  dff1o6  5609  oprabid  5735  mpo2eqb  5812  ralrnmpo  5817  rexrnmpo  5818  opabex3d  5950  opabex3  5951  xporderlem  6058  f1od2  6062  tfr0dm  6149  tfrexlem  6161  frec0g  6224  nnaord  6335  ecid  6422  mptelixpg  6558  elixpsn  6559  mapsnen  6635  xpsnen  6644  xpcomco  6649  xpassen  6653  nqnq0  7150  opelreal  7515  pitoregt0  7536  elnn0  8831  elxnn0  8894  elxr  9404  xrnepnf  9406  elfzuzb  9641  4fvwrd4  9758  elfzo2  9768  resqrexlemsqa  10636  fisumcom2  11046  modfsummod  11066  isprm2  11591  isprm4  11593  ntreq0  12083  txbas  12208  metrest  12434