Theorem 3bitr4i 212

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

Syntax hints:   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bibi2d  232  pm4.71  389  pm5.32ri  455  mpan10  474  an31  564  an4  586  or4  776  ordir  822  andir  824  3anrot  1007  3orrot  1008  3ancoma  1009  3orcomb  1011  3ioran  1017  3anbi123i  1212  3orbi123i  1213  3or6  1357  xorcom  1430  nfbii  1519  19.26-3an  1529  alnex  1545  19.42h  1733  19.42  1734  equsal  1773  equsalv  1839  sb6  1933  eeeanv  1984  sbbi  2010  sbco3xzyz  2024  sbcom2v  2036  sbel2x  2049  sb8eu  2090  sb8mo  2091  sb8euh  2100  eu1  2102  cbvmo  2117  mo3h  2131  sbmo  2137  eqcom  2231  abeq1  2339  cbvabw  2352  cbvab  2353  clelab  2355  nfceqi  2368  sbabel  2399  ralbii2  2540  rexbii2  2541  r2alf  2547  r2exf  2548  nfraldya  2565  nfrexdya  2566  r3al  2574  r19.41  2686  r19.42v  2688  ralcomf  2692  rexcomf  2693  reean  2700  3reeanv  2702  rabid2  2708  rabbi  2709  cbvrmow  2714  reubiia  2717  rmobiia  2722  reu5  2749  rmo5  2752  cbvralfw  2754  cbvrexfw  2755  cbvralf  2756  cbvrexf  2757  cbvreuw  2760  cbvreu  2763  cbvrmo  2764  cbvralvw  2769  cbvrexvw  2770  vjust  2801  ceqsex3v  2844  ceqsex4v  2845  ceqsex8v  2847  eueq  2975  reu2  2992  reu6  2993  reu3  2994  rmo4  2997  rmo3f  3001  2rmorex  3010  cbvsbcw  3057  cbvsbc  3058  sbccomlem  3104  rmo3  3122  csbcow  3136  csbabg  3187  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  eqss  3240  uniiunlem  3314  ssequn1  3375  unss  3379  rexun  3385  ralunb  3386  elin3  3396  incom  3397  inass  3415  ssin  3427  ssddif  3439  unssdif  3440  difin  3442  invdif  3447  indif  3448  indi  3452  symdifxor  3471  disj3  3545  eldifpr  3694  rexsns  3706  reusn  3740  prss  3827  tpss  3839  eluni2  3895  elunirab  3904  uniun  3910  uni0b  3916  unissb  3921  elintrab  3938  ssintrab  3949  intun  3957  intpr  3958  iuncom  3974  iuncom4  3975  iunab  4015  ssiinf  4018  iinab  4030  iunin2  4032  iunun  4047  iunxun  4048  iunxiun  4050  sspwuni  4053  iinpw  4059  cbvdisj  4072  brun  4138  brin  4139  brdif  4140  dftr2  4187  inuni  4243  repizf2lem  4249  unidif0  4255  ssext  4311  pweqb  4313  otth2  4331  opelopabsbALT  4351  eqopab2b  4372  pwin  4377  unisuc  4508  elpwpwel  4570  sucexb  4593  elomssom  4701  xpiundi  4782  xpiundir  4783  poinxp  4793  soinxp  4794  seinxp  4795  inopab  4860  difopab  4861  raliunxp  4869  rexiunxp  4870  iunxpf  4876  cnvco  4913  dmiun  4938  dmuni  4939  dm0rn0  4946  brres  5017  dmres  5032  restidsing  5067  cnvsym  5118  asymref  5120  codir  5123  qfto  5124  cnvopab  5136  cnvdif  5141  rniun  5145  dminss  5149  imainss  5150  cnvcnvsn  5211  resco  5239  imaco  5240  rnco  5241  coiun  5244  coass  5253  ressn  5275  cnviinm  5276  xpcom  5281  funcnv  5388  funcnv3  5389  fncnv  5393  fun11  5394  fnres  5446  dfmpt3  5452  fnopabg  5453  fintm  5519  fin  5520  fores  5566  dff1o3  5586  fun11iun  5601  f11o  5613  f1ompt  5794  fsn  5815  imaiun  5896  isores2  5949  eqoprab2b  6074  opabex3d  6278  opabex3  6279  dfopab2  6347  dfoprab3s  6348  fmpox  6360  tpostpos  6425  dfsmo2  6448  qsid  6764  mapval2  6842  mapsncnv  6859  elixp2  6866  ixpin  6887  xpassen  7009  diffitest  7069  pw1dc0el  7096  supmoti  7183  eqinfti  7210  distrnqg  7597  ltbtwnnq  7626  distrnq0  7669  nqprrnd  7753  ltresr  8049  elznn0nn  9483  xrnemnf  10002  xrnepnf  10003  elioomnf  10193  elxrge0  10203  elfzuzb  10244  fzass4  10287  elfz2nn0  10337  elfzo2  10375  elfzo3  10389  lbfzo0  10410  fzind2  10475  infssuzex  10483  dfrp2  10513  rexfiuz  11540  fisumcom2  11989  prodmodc  12129  fprodcom2fi  12177  4sqlem12  12965  infpn2  13067  xpsfrnel  13417  xpscf  13420  islmod  14295  isbasis2g  14759  tgval2  14765  ntreq0  14846  txuni2  14970  isms2  15168  plyun0  15450  bdceq  16373