Theorem 3bitr4i 210

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	⊢ (𝜑 ↔ 𝜓)
3bitr4i.2	⊢ (𝜒 ↔ 𝜑)
3bitr4i.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3bitr4i	⊢ (𝜒 ↔ 𝜃)

Proof of Theorem 3bitr4i

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 185	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 182	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bibi2d  230  pm4.71  381  pm5.32ri  443  mpan10  458  an31  529  an4  551  or4  721  ordir  764  andir  766  dcbii  783  3anrot  927  3orrot  928  3ancoma  929  3orcomb  931  3ioran  937  3anbi123i  1130  3orbi123i  1131  3or6  1257  xorcom  1322  nfbii  1405  19.26-3an  1415  alnex  1431  19.42h  1620  19.42  1621  equsal  1659  sb6  1811  eeeanv  1853  sbbi  1878  sbco3xzyz  1892  sbcom2v  1906  sbel2x  1919  sb8eu  1958  sb8mo  1959  sb8euh  1968  eu1  1970  cbvmo  1985  mo3h  1998  sbmo  2004  eqcom  2087  abeq1  2194  cbvab  2207  clelab  2209  nfceqi  2221  sbabel  2250  ralbii2  2384  rexbii2  2385  r2alf  2391  r2exf  2392  nfraldya  2408  nfrexdya  2409  r3al  2416  r19.41  2518  r19.42v  2520  ralcomf  2524  rexcomf  2525  reean  2531  3reeanv  2533  rabid2  2539  rabbi  2540  reubiia  2547  rmobiia  2552  reu5  2575  rmo5  2578  cbvralf  2580  cbvrexf  2581  cbvreu  2584  cbvrmo  2585  vjust  2616  ceqsex3v  2655  ceqsex4v  2656  ceqsex8v  2658  eueq  2777  reu2  2794  reu6  2795  reu3  2796  rmo4  2799  2rmorex  2810  cbvsbc  2856  sbccomlem  2902  rmo3  2919  csbabg  2978  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  eqss  3029  uniiunlem  3098  ssequn1  3159  unss  3163  rexun  3169  ralunb  3170  elin3  3180  incom  3181  inass  3199  ssin  3211  ssddif  3222  unssdif  3223  difin  3225  invdif  3230  indif  3231  indi  3235  symdifxor  3254  disj3  3323  rexsns  3465  reusn  3496  prss  3576  tpss  3585  eluni2  3640  elunirab  3649  uniun  3655  uni0b  3661  unissb  3666  elintrab  3683  ssintrab  3694  intun  3702  intpr  3703  iuncom  3719  iuncom4  3720  iunab  3759  ssiinf  3762  iinab  3774  iunin2  3776  iunun  3790  iunxun  3791  iunxiun  3792  sspwuni  3795  iinpw  3798  cbvdisj  3811  brun  3866  brin  3867  brdif  3868  dftr2  3913  inuni  3966  repizf2lem  3971  unidif0  3977  ssext  4022  pweqb  4024  otth2  4042  opelopabsbALT  4060  eqopab2b  4080  pwin  4083  unisuc  4214  sucexb  4287  elnn  4393  xpiundi  4464  xpiundir  4465  poinxp  4475  soinxp  4476  seinxp  4477  inopab  4536  difopab  4537  raliunxp  4545  rexiunxp  4546  iunxpf  4552  cnvco  4589  dmiun  4613  dmuni  4614  dm0rn0  4621  brres  4687  dmres  4701  cnvsym  4782  asymref  4784  codir  4787  qfto  4788  cnvopab  4800  cnvdif  4804  rniun  4808  dminss  4812  imainss  4813  cnvcnvsn  4873  resco  4901  imaco  4902  rnco  4903  coiun  4906  coass  4915  ressn  4937  cnviinm  4938  xpcom  4943  funcnv  5040  funcnv3  5041  fncnv  5045  fun11  5046  fnres  5095  dfmpt3  5101  fnopabg  5102  fintm  5159  fin  5160  fores  5205  dff1o3  5222  fun11iun  5237  f11o  5249  f1ompt  5413  fsn  5432  imaiun  5500  isores2  5553  eqoprab2b  5664  opabex3d  5849  opabex3  5850  dfopab2  5916  dfoprab3s  5917  fmpt2x  5927  tpostpos  5983  dfsmo2  6006  qsid  6309  mapval2  6387  mapsncnv  6404  xpassen  6498  diffitest  6555  supmoti  6632  eqinfti  6659  distrnqg  6890  ltbtwnnq  6919  distrnq0  6962  nqprrnd  7046  ltresr  7320  elznn0nn  8697  xrnemnf  9180  xrnepnf  9181  elioomnf  9318  elxrge0  9328  elfzuzb  9366  fzass4  9407  elfz2nn0  9456  elfzo2  9489  elfzo3  9502  lbfzo0  9520  fzind2  9578  rexfiuz  10317  infssuzex  10820  bdceq  11171