Theorem 3bitri 262

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 240	. 2 |- (ps <-> th)
5	1, 4	bitri 240	1 |- (ph <-> th)

Syntax hints:   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bibi1i  305  orbi1i  506  orass  510  or32  513  pm5.32  617  an32  773  excxor  1309  trunanfal  1355  falxortru  1360  nic-axALT  1439  tbw-bijust  1463  rb-bijust  1514  19.43  1605  19.43OLD  1606  excom13  1743  nf4  1868  19.12vv  1898  3exdistr  1910  4exdistr  1911  eeeanv  1914  ee4anv  1915  sb3an  2070  sbnf2  2108  sb8eu  2222  2eu4  2287  2eu7  2290  2eu8  2291  r19.26-3  2749  rexcom13  2774  cbvreu  2834  ceqsex2  2896  ceqsex4v  2899  ralrab2  3003  rexrab2  3005  reu2  3025  rmo4  3030  reu8  3033  2reu5lem3  3044  rmo2  3132  rmo3  3134  eldif  3222  ss2rab  3343  rabss  3344  ssrab  3345  dfss4  3490  undi  3503  undif3  3516  difin2  3517  dfnul2  3553  disj4  3600  elimif  3692  disjsn  3787  ssunpr  3869  sspr  3870  sstp  3871  uni0b  3917  uni0c  3918  ssint  3943  iunss  4008  iundif2  4034  nincompl  4073  elpw12  4146  elpw11c  4148  eluni1g  4173  eqrelk  4213  opkelcokg  4262  opkelimagekg  4272  imacok  4283  sikexlem  4296  dfimak2  4299  dfpw12  4302  dfint3  4319  unipw1  4326  dfpw2  4328  sb8iota  4347  dfaddc2  4382  addcid1  4406  nnsucelrlem2  4426  nndisjeq  4430  ltfinex  4465  ssfin  4471  eqpwrelk  4479  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnadjoinpw  4522  nnpweqlem1  4523  nnpweq  4524  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  tfinnn  4535  spfinex  4538  vfinspsslem1  4551  dfop2lem1  4574  proj1op  4601  eqvinop  4607  opeq  4620  opeqexb  4621  brabsb  4699  opelopabf  4712  opabn0  4717  br1stg  4731  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem6  4737  dfswap2  4742  dfid3  4769  xpiundi  4818  opeliunxp  4821  ssopr  4847  cnvuni  4896  elrn  4897  dmuni  4915  dmopab3  4918  elima1c  4948  elimapw11c  4949  brres  4950  elsnres  4997  intirr  5030  rnuni  5039  xpeq0  5047  ssrnres  5060  dminxp  5062  dmsnopg  5067  cnvresima  5078  imaco  5087  rnco  5088  coi1  5095  elxp4  5109  dffun2  5120  fun11  5160  fnres  5200  f1funfun  5264  dff1o2  5292  dff1o4  5295  eqfnfv3  5395  fnressn  5439  dff13  5472  dff1o6  5476  cnvswap  5511  cnvsi  5519  oprabid  5551  brco1st  5778  brco2nd  5779  trtxp  5782  elfix  5788  brimage  5794  oqelins4  5795  otsnelsi3  5806  releqmpt2  5810  composeex  5821  addcfnex  5825  funsex  5829  brpprod  5840  dmpprod  5841  crossex  5851  pw1fnf1o  5856  fvfullfunlem1  5862  transex  5911  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  eqerlem  5961  fundmen  6044  xpassenlem  6057  xpassen  6058  enpw1lem1  6062  enmap2lem1  6064  enmap1lem1  6070  enpw1pw  6076  enprmaplem1  6077  lecex  6116  ovmuc  6131  mucex  6134  ovcelem1  6172  ceex  6175  ce0nn  6181  el2c  6192  dflec3  6222  taddc  6230  tcfnex  6245  addccan2nclem1  6264  addccan2nclem2  6265  nmembers1lem1  6269  nncdiv3lem1  6276  nncdiv3lem2  6277  nnc3n3p1  6279  spacvallem1  6282  nchoicelem10  6299  nchoicelem11  6300  nchoicelem16  6305