Theorem 3bitr4i 268

Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3bitr4i.1	|- (ph <-> ps)
3bitr4i.2	|- (ch <-> ph)
3bitr4i.3	|- (th <-> ps)

Assertion

Ref	Expression
3bitr4i	|- (ch <-> th)

Proof of Theorem 3bitr4i

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 |- (ch <-> ph)
2		3bitr4i.1	. . 3 |- (ph <-> ps)
3		3bitr4i.3	. . 3 |- (th <-> ps)
4	2, 3	bitr4i 243	. 2 |- (ph <-> th)
5	1, 4	bitri 240	1 |- (ch <-> 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:  bibi2d  309  or4  514  pm4.14  561  pm4.71  611  pm5.32ri  619  an31  775  an4  797  orimdi  820  ordi  834  ordir  835  andir  838  dfbi3  863  orbidi  898  3anrot  939  3orrot  940  3ancoma  941  3orcoma  942  3orcomb  944  3ioran  950  3anbi123i  1140  3orbi123i  1141  an6  1261  3or6  1263  nancom  1290  xorcom  1307  xorass  1308  xorneg2  1312  xorbi12i  1314  hadbi  1387  hadcoma  1388  hadcomb  1389  cador  1391  cadan  1392  hadnot  1393  cadnot  1394  cadcoma  1395  cadcomb  1396  cad1  1398  nic-axALT  1439  nfbii  1569  19.26-3an  1595  19.43OLD  1606  cbvexvw  1703  excom  1741  equsalhw  1838  19.32  1875  19.31  1876  19.42  1880  eeeanv  1914  equsex  1962  cbvex  1985  dfsb3  2056  sbor  2066  sban  2069  sbbi  2071  sb8e  2093  sb6  2099  pm11.07  2115  sbel2x  2125  sbex  2128  sb8eu  2222  sb8mo  2223  eu1  2225  sbmo  2234  cbvmo  2241  moanim  2260  eqcom  2355  abeq1  2459  cbvab  2471  clelab  2473  nfceqi  2485  sbabel  2515  ralbii2  2642  rexbii2  2643  r2alf  2649  r2exf  2650  r3al  2671  r19.30  2756  r19.32v  2757  r19.41  2763  r19.42v  2765  r19.43  2766  ralcomf  2769  rexcomf  2770  reean  2777  3reeanv  2779  2ralor  2780  rabid2  2788  rabbi  2789  reubiia  2796  rmobiia  2801  reu5  2824  rmo5  2827  cbvralf  2829  cbvrexf  2830  cbvreu  2833  cbvrmo  2834  vjust  2860  ceqsex3v  2897  ceqsex4v  2898  ceqsex8v  2900  eueq  3008  reu2  3024  reu6  3025  reu3  3026  rmo4  3029  2reu5  3044  cbvsbc  3074  sbccomlem  3116  rmo3  3133  csbabg  3197  cbvralcsf  3198  cbvrexcsf  3199  cbvreucsf  3200  elsymdif  3223  nincom  3226  eqss  3287  uniiunlem  3353  sspsstri  3371  ssequn1  3433  unss  3437  rexun  3443  ralunb  3444  elin3  3447  incom  3448  inass  3465  ssin  3477  nssinpss  3487  dfun2  3490  difin  3492  indi  3501  indifdir  3511  symdif2  3520  complab  3524  rabn0  3570  disj  3591  disj3  3595  ssdif0  3609  inssdif0  3617  ssundif  3633  sscon34  3661  dfif2  3664  snprc  3788  reusn  3793  difsnpss  3851  prss  3861  tpss  3871  pwpr  3883  disj5  3890  eluni2  3895  elunirab  3904  unipr  3905  uniun  3910  unissb  3921  elintrab  3938  ssintrab  3949  intun  3958  intpr  3959  iuncom  3975  iuncom4  3976  iunab  4012  ssiinf  4015  iunn0  4026  iinab  4027  iunin2  4030  iinun2  4032  iundif2  4033  iunun  4046  iunxun  4047  iunxiun  4048  iinuni  4049  sspwuni  4051  iinpw  4054  pwadjoin  4119  elpw12  4145  snelpw1  4146  pw1un  4163  pw1in  4164  pw1sn  4165  pw111  4170  opkelcokg  4261  cnvkxpk  4276  inxpk  4277  imacok  4282  dfuni12  4291  dfimak2  4298  insklem  4304  dfidk2  4313  dfint3  4318  ndisjrelk  4323  unipw1  4325  dfpw2  4327  dfeu2  4333  dfaddc2  4381  dfnnc2  4395  addcid1  4405  elsuc  4413  addcass  4415  nncaddccl  4419  nnsucelrlem1  4424  nndisjeq  4429  preaddccan2lem1  4454  ltfinex  4464  ltfintrilem1  4465  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenoddnnnul  4514  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  vfinspclt  4552  dfphi2  4569  dfop2lem1  4573  dfproj22  4577  proj1op  4600  proj2op  4601  phialllem1  4616  opeqexb  4620  brun  4692  brin  4693  brdif  4694  setconslem1  4731  setconslem2  4732  setconslem4  4734  setconslem6  4736  dfswap2  4741  opelxp  4811  xpiundi  4817  xpiundir  4818  raliunxp  4823  rexiunxp  4824  rexxpf  4828  iunxpf  4829  brinxp2  4835  eqrel  4845  eqopr  4847  inopab  4862  dmun  4912  dmuni  4914  dm0rn0  4921  elres  4995  cnvsym  5027  cnvopab  5030  cnvdif  5034  rnuni  5038  dminss  5041  imainss  5042  dmsnopg  5066  cnvsn  5073  rnsnop  5075  resco  5085  imaco  5086  rnco  5087  coiun  5090  coass  5097  df2nd2  5111  dfxp2  5113  cnviin  5118  dffun7  5133  funcnv  5156  funcnv3  5157  fncnv  5158  fun11  5159  imadif  5171  fnres  5199  fnopabg  5205  fint  5245  fin  5246  fores  5278  dff1o2  5291  dff1o3  5292  f1orn  5296  fun11iun  5305  f11o  5315  fsn  5432  imaiun  5464  isores2  5493  isomin  5496  opbr1st  5501  opbr2nd  5502  dfid4  5503  dfdm4  5507  dfrn5  5508  cnvswap  5510  swapf1o  5511  cnvsi  5518  dmsi  5519  eloprabga  5578  fmpt2x  5730  brtxp  5783  restxp  5786  brimage  5793  oqelins4  5794  dmtxp  5802  txpcofun  5803  releqel  5807  cupex  5816  disjex  5823  addcfnex  5824  epprc  5827  funsex  5828  fnsex  5832  brpprod  5839  dmpprod  5840  crossex  5850  pw1fnex  5852  pw1fnf1o  5855  domfnex  5870  ranfnex  5871  clos1induct  5880  transex  5910  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  porta  5933  frds  5935  elec  5964  qsexg  5982  qsid  5990  mapexi  6003  mapval2  6018  map0e  6023  enex  6031  xpassenlem  6056  xpassen  6057  enmap2lem1  6063  enprmaplem4  6079  nenpw1pwlem1  6084  lecex  6115  ncseqnc  6128  mucex  6133  ncpw1  6152  ovcelem1  6171  ceexlem1  6173  ceex  6174  ce0nn  6180  el2c  6191  tcfnex  6244  nmembers1lem1  6268  nncdiv3lem1  6275  nncdiv3lem2  6276  nncdiv3  6277  spacvallem1  6281  nchoicelem10  6298  nchoicelem11  6299  nchoicelem18  6306  fnfreclem1  6317  fnfreclem2  6318