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-mp 5  ax-1 6  ax-2 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  386  pm5.32ri  450  mpan10  465  an31  553  an4  575  or4  760  ordir  806  andir  808  3anrot  967  3orrot  968  3ancoma  969  3orcomb  971  3ioran  977  3anbi123i  1170  3orbi123i  1171  3or6  1301  xorcom  1366  nfbii  1449  19.26-3an  1459  alnex  1475  19.42h  1665  19.42  1666  equsal  1705  sb6  1858  eeeanv  1903  sbbi  1930  sbco3xzyz  1944  sbcom2v  1958  sbel2x  1971  sb8eu  2010  sb8mo  2011  sb8euh  2020  eu1  2022  cbvmo  2037  mo3h  2050  sbmo  2056  eqcom  2139  abeq1  2247  cbvabw  2260  cbvab  2261  clelab  2263  nfceqi  2275  sbabel  2305  ralbii2  2443  rexbii2  2444  r2alf  2450  r2exf  2451  nfraldya  2467  nfrexdya  2468  r3al  2475  r19.41  2584  r19.42v  2586  ralcomf  2590  rexcomf  2591  reean  2597  3reeanv  2599  rabid2  2605  rabbi  2606  reubiia  2613  rmobiia  2618  reu5  2641  rmo5  2644  cbvralf  2646  cbvrexf  2647  cbvreu  2650  cbvrmo  2651  vjust  2682  ceqsex3v  2723  ceqsex4v  2724  ceqsex8v  2726  eueq  2850  reu2  2867  reu6  2868  reu3  2869  rmo4  2872  rmo3f  2876  2rmorex  2885  cbvsbcw  2931  cbvsbc  2932  sbccomlem  2978  rmo3  2995  csbabg  3056  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  eqss  3107  uniiunlem  3180  ssequn1  3241  unss  3245  rexun  3251  ralunb  3252  elin3  3262  incom  3263  inass  3281  ssin  3293  ssddif  3305  unssdif  3306  difin  3308  invdif  3313  indif  3314  indi  3318  symdifxor  3337  disj3  3410  rexsns  3558  reusn  3589  prss  3671  tpss  3680  eluni2  3735  elunirab  3744  uniun  3750  uni0b  3756  unissb  3761  elintrab  3778  ssintrab  3789  intun  3797  intpr  3798  iuncom  3814  iuncom4  3815  iunab  3854  ssiinf  3857  iinab  3869  iunin2  3871  iunun  3886  iunxun  3887  iunxiun  3889  sspwuni  3892  iinpw  3898  cbvdisj  3911  brun  3974  brin  3975  brdif  3976  dftr2  4023  inuni  4075  repizf2lem  4080  unidif0  4086  ssext  4138  pweqb  4140  otth2  4158  opelopabsbALT  4176  eqopab2b  4196  pwin  4199  unisuc  4330  elpwpwel  4391  sucexb  4408  elnn  4514  xpiundi  4592  xpiundir  4593  poinxp  4603  soinxp  4604  seinxp  4605  inopab  4666  difopab  4667  raliunxp  4675  rexiunxp  4676  iunxpf  4682  cnvco  4719  dmiun  4743  dmuni  4744  dm0rn0  4751  brres  4820  dmres  4835  cnvsym  4917  asymref  4919  codir  4922  qfto  4923  cnvopab  4935  cnvdif  4940  rniun  4944  dminss  4948  imainss  4949  cnvcnvsn  5010  resco  5038  imaco  5039  rnco  5040  coiun  5043  coass  5052  ressn  5074  cnviinm  5075  xpcom  5080  funcnv  5179  funcnv3  5180  fncnv  5184  fun11  5185  fnres  5234  dfmpt3  5240  fnopabg  5241  fintm  5303  fin  5304  fores  5349  dff1o3  5366  fun11iun  5381  f11o  5393  f1ompt  5564  fsn  5585  imaiun  5654  isores2  5707  eqoprab2b  5822  opabex3d  6012  opabex3  6013  dfopab2  6080  dfoprab3s  6081  fmpox  6091  tpostpos  6154  dfsmo2  6177  qsid  6487  mapval2  6565  mapsncnv  6582  elixp2  6589  ixpin  6610  xpassen  6717  diffitest  6774  supmoti  6873  eqinfti  6900  distrnqg  7188  ltbtwnnq  7217  distrnq0  7260  nqprrnd  7344  ltresr  7640  elznn0nn  9061  xrnemnf  9557  xrnepnf  9558  elioomnf  9744  elxrge0  9754  elfzuzb  9793  fzass4  9835  elfz2nn0  9885  elfzo2  9920  elfzo3  9933  lbfzo0  9951  fzind2  10009  rexfiuz  10754  fisumcom2  11200  infssuzex  11631  isbasis2g  12201  tgval2  12209  ntreq0  12290  txuni2  12414  isms2  12612  bdceq  13029