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  eqabcb  2460  cbvab  2472  clelab  2474  nfceqi  2486  sbabel  2516  ralbii2  2643  rexbii2  2644  r2alf  2650  r2exf  2651  r3al  2672  r19.30  2757  r19.32v  2758  r19.41  2764  r19.42v  2766  r19.43  2767  ralcomf  2770  rexcomf  2771  reean  2778  3reeanv  2780  2ralor  2781  rabid2  2789  reubiia  2797  rmobiia  2802  reu5  2825  rmo5  2828  cbvralf  2830  cbvrexf  2831  cbvreu  2834  cbvrmo  2835  vjust  2861  ceqsex3v  2898  ceqsex4v  2899  ceqsex8v  2901  eueq  3009  reu2  3025  reu6  3026  reu3  3027  rmo4  3030  2reu5  3045  cbvsbc  3075  sbccomlem  3117  rmo3  3134  csbabg  3198  cbvralcsf  3199  cbvrexcsf  3200  cbvreucsf  3201  elsymdif  3224  nincom  3227  eqss  3288  uniiunlem  3354  sspsstri  3372  ssequn1  3434  unss  3438  rexun  3444  ralunb  3445  elin3  3448  incom  3449  inass  3466  ssin  3478  nssinpss  3488  dfun2  3491  difin  3493  indi  3502  indifdir  3512  symdif2  3521  complab  3525  rabn0  3571  disj  3592  disj3  3596  ssdif0  3610  inssdif0  3618  ssundif  3634  sscon34  3662  dfif2  3665  snprc  3789  reusn  3794  difsnpss  3852  prss  3862  tpss  3872  pwpr  3884  disj5  3891  eluni2  3896  elunirab  3905  unipr  3906  uniun  3911  unissb  3922  elintrab  3939  ssintrab  3950  intun  3959  intpr  3960  iuncom  3976  iuncom4  3977  iunab  4013  ssiinf  4016  iunn0  4027  iinab  4028  iunin2  4031  iinun2  4033  iundif2  4034  iunun  4047  iunxun  4048  iunxiun  4049  iinuni  4050  sspwuni  4052  iinpw  4055  pwadjoin  4120  elpw12  4146  snelpw1  4147  pw1un  4164  pw1in  4165  pw1sn  4166  pw111  4171  opkelcokg  4262  cnvkxpk  4277  inxpk  4278  imacok  4283  dfuni12  4292  dfimak2  4299  insklem  4305  dfidk2  4314  dfint3  4319  ndisjrelk  4324  unipw1  4326  dfpw2  4328  dfeu2  4334  dfaddc2  4382  dfnnc2  4396  addcid1  4406  elsuc  4414  addcass  4416  nncaddccl  4420  nnsucelrlem1  4425  nndisjeq  4430  preaddccan2lem1  4455  ltfinex  4465  ltfintrilem1  4466  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenoddnnnul  4515  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  vfinspclt  4553  dfphi2  4570  dfop2lem1  4574  dfproj22  4578  proj1op  4601  proj2op  4602  phialllem1  4617  opeqexb  4621  brun  4693  brin  4694  brdif  4695  setconslem1  4732  setconslem2  4733  setconslem4  4735  setconslem6  4737  dfswap2  4742  opelxp  4812  xpiundi  4818  xpiundir  4819  raliunxp  4824  rexiunxp  4825  rexxpf  4829  iunxpf  4830  brinxp2  4836  eqrel  4846  eqopr  4848  inopab  4863  dmun  4913  dmuni  4915  dm0rn0  4922  elres  4996  cnvsym  5028  cnvopab  5031  cnvdif  5035  rnuni  5039  dminss  5042  imainss  5043  dmsnopg  5067  cnvsn  5074  rnsnop  5076  resco  5086  imaco  5087  rnco  5088  coiun  5091  coass  5098  df2nd2  5112  dfxp2  5114  cnviin  5119  dffun7  5134  funcnv  5157  funcnv3  5158  fncnv  5159  fun11  5160  imadif  5172  fnres  5200  fnopabg  5206  fint  5246  fin  5247  fores  5279  dff1o2  5292  dff1o3  5293  f1orn  5297  fun11iun  5306  f11o  5316  fsn  5433  imaiun  5465  isores2  5494  isomin  5497  opbr1st  5502  opbr2nd  5503  dfid4  5504  dfdm4  5508  dfrn5  5509  cnvswap  5511  swapf1o  5512  cnvsi  5519  dmsi  5520  eloprabga  5579  fmpt2x  5731  brtxp  5784  restxp  5787  brimage  5794  oqelins4  5795  dmtxp  5803  txpcofun  5804  releqel  5808  cupex  5817  disjex  5824  addcfnex  5825  epprc  5828  funsex  5829  fnsex  5833  brpprod  5840  dmpprod  5841  crossex  5851  pw1fnex  5853  pw1fnf1o  5856  domfnex  5871  ranfnex  5872  clos1induct  5881  transex  5911  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  porta  5934  frds  5936  elec  5965  qsexg  5983  qsid  5991  mapexi  6004  mapval2  6019  map0e  6024  enex  6032  xpassenlem  6057  xpassen  6058  enmap2lem1  6064  enprmaplem4  6080  nenpw1pwlem1  6085  lecex  6116  ncseqnc  6129  mucex  6134  ncpw1  6153  ovcelem1  6172  ceexlem1  6174  ceex  6175  ce0nn  6181  el2c  6192  tcfnex  6245  nmembers1lem1  6269  nncdiv3lem1  6276  nncdiv3lem2  6277  nncdiv3  6278  spacvallem1  6282  nchoicelem10  6299  nchoicelem11  6300  nchoicelem18  6307  fnfreclem1  6318  fnfreclem2  6319