Theorem 3bitr4i 211

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 186	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 183	1 ⊢ (𝜒 ↔ 𝜃)

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:  bibi2d  231  pm4.71  384  pm5.32ri  448  mpan10  463  an31  536  an4  558  or4  743  ordir  789  andir  791  3anrot  948  3orrot  949  3ancoma  950  3orcomb  952  3ioran  958  3anbi123i  1151  3orbi123i  1152  3or6  1282  xorcom  1347  nfbii  1430  19.26-3an  1440  alnex  1456  19.42h  1646  19.42  1647  equsal  1686  sb6  1838  eeeanv  1881  sbbi  1906  sbco3xzyz  1920  sbcom2v  1934  sbel2x  1947  sb8eu  1986  sb8mo  1987  sb8euh  1996  eu1  1998  cbvmo  2013  mo3h  2026  sbmo  2032  eqcom  2115  abeq1  2222  cbvab  2235  clelab  2237  nfceqi  2249  sbabel  2279  ralbii2  2417  rexbii2  2418  r2alf  2424  r2exf  2425  nfraldya  2441  nfrexdya  2442  r3al  2449  r19.41  2558  r19.42v  2560  ralcomf  2564  rexcomf  2565  reean  2571  3reeanv  2573  rabid2  2579  rabbi  2580  reubiia  2587  rmobiia  2592  reu5  2615  rmo5  2618  cbvralf  2620  cbvrexf  2621  cbvreu  2624  cbvrmo  2625  vjust  2656  ceqsex3v  2697  ceqsex4v  2698  ceqsex8v  2700  eueq  2822  reu2  2839  reu6  2840  reu3  2841  rmo4  2844  rmo3f  2848  2rmorex  2857  cbvsbc  2903  sbccomlem  2949  rmo3  2966  csbabg  3025  cbvralcsf  3026  cbvrexcsf  3027  cbvreucsf  3028  eqss  3076  uniiunlem  3149  ssequn1  3210  unss  3214  rexun  3220  ralunb  3221  elin3  3231  incom  3232  inass  3250  ssin  3262  ssddif  3274  unssdif  3275  difin  3277  invdif  3282  indif  3283  indi  3287  symdifxor  3306  disj3  3379  rexsns  3527  reusn  3558  prss  3640  tpss  3649  eluni2  3704  elunirab  3713  uniun  3719  uni0b  3725  unissb  3730  elintrab  3747  ssintrab  3758  intun  3766  intpr  3767  iuncom  3783  iuncom4  3784  iunab  3823  ssiinf  3826  iinab  3838  iunin2  3840  iunun  3855  iunxun  3856  iunxiun  3858  sspwuni  3861  iinpw  3867  cbvdisj  3880  brun  3939  brin  3940  brdif  3941  dftr2  3986  inuni  4038  repizf2lem  4043  unidif0  4049  ssext  4101  pweqb  4103  otth2  4121  opelopabsbALT  4139  eqopab2b  4159  pwin  4162  unisuc  4293  elpwpwel  4354  sucexb  4371  elnn  4477  xpiundi  4555  xpiundir  4556  poinxp  4566  soinxp  4567  seinxp  4568  inopab  4629  difopab  4630  raliunxp  4638  rexiunxp  4639  iunxpf  4645  cnvco  4682  dmiun  4706  dmuni  4707  dm0rn0  4714  brres  4781  dmres  4796  cnvsym  4878  asymref  4880  codir  4883  qfto  4884  cnvopab  4896  cnvdif  4901  rniun  4905  dminss  4909  imainss  4910  cnvcnvsn  4971  resco  4999  imaco  5000  rnco  5001  coiun  5004  coass  5013  ressn  5035  cnviinm  5036  xpcom  5041  funcnv  5140  funcnv3  5141  fncnv  5145  fun11  5146  fnres  5195  dfmpt3  5201  fnopabg  5202  fintm  5264  fin  5265  fores  5310  dff1o3  5327  fun11iun  5342  f11o  5354  f1ompt  5523  fsn  5544  imaiun  5613  isores2  5666  eqoprab2b  5781  opabex3d  5971  opabex3  5972  dfopab2  6039  dfoprab3s  6040  fmpox  6050  tpostpos  6113  dfsmo2  6136  qsid  6446  mapval2  6524  mapsncnv  6541  elixp2  6548  ixpin  6569  xpassen  6675  diffitest  6732  supmoti  6830  eqinfti  6857  distrnqg  7137  ltbtwnnq  7166  distrnq0  7209  nqprrnd  7293  ltresr  7568  elznn0nn  8966  xrnemnf  9451  xrnepnf  9452  elioomnf  9638  elxrge0  9648  elfzuzb  9687  fzass4  9729  elfz2nn0  9779  elfzo2  9814  elfzo3  9827  lbfzo0  9845  fzind2  9903  rexfiuz  10647  fisumcom2  11093  infssuzex  11484  isbasis2g  12049  tgval2  12057  ntreq0  12138  txuni2  12261  isms2  12437  bdceq  12723