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  566  an4  588  or4  779  ordir  825  andir  827  3anrot  1010  3orrot  1011  3ancoma  1012  3orcomb  1014  3ioran  1020  3anbi123i  1215  3orbi123i  1216  3or6  1360  xorcom  1433  nfbii  1522  19.26-3an  1532  alnex  1548  19.42h  1735  19.42  1736  equsal  1775  equsalv  1841  sb6  1935  eeeanv  1986  sbbi  2012  sbco3xzyz  2026  sbcom2v  2038  sbel2x  2051  sb8eu  2092  sb8mo  2093  sb8euh  2102  eu1  2104  cbvmo  2119  mo3h  2133  sbmo  2139  eqcom  2233  abeq1  2341  cbvabw  2355  cbvab  2356  clelab  2358  nfceqi  2371  sbabel  2402  ralbii2  2543  rexbii2  2544  r2alf  2550  r2exf  2551  nfraldya  2568  nfrexdya  2569  r3al  2577  r19.41  2689  r19.42v  2691  ralcomf  2695  rexcomf  2696  reean  2703  3reeanv  2705  rabid2  2711  rabbi  2712  cbvrmow  2717  reubiia  2720  rmobiia  2725  reu5  2752  rmo5  2755  cbvralfw  2757  cbvrexfw  2758  cbvralf  2759  cbvrexf  2760  cbvreuw  2763  cbvreu  2766  cbvrmo  2767  cbvralvw  2772  cbvrexvw  2773  vjust  2804  ceqsex3v  2847  ceqsex4v  2848  ceqsex8v  2850  eueq  2978  reu2  2995  reu6  2996  reu3  2997  rmo4  3000  rmo3f  3004  2rmorex  3013  cbvsbcw  3060  cbvsbc  3061  sbccomlem  3107  rmo3  3125  csbcow  3139  csbabg  3190  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  eqss  3243  uniiunlem  3318  ssequn1  3379  unss  3383  rexun  3389  ralunb  3390  elin3  3400  incom  3401  inass  3419  ssin  3431  ssddif  3443  unssdif  3444  difin  3446  invdif  3451  indif  3452  indi  3456  symdifxor  3475  disj3  3549  eldifpr  3700  rexsns  3712  reusn  3746  prss  3834  tpss  3846  eluni2  3902  elunirab  3911  uniun  3917  uni0b  3923  unissb  3928  elintrab  3945  ssintrab  3956  intun  3964  intpr  3965  iuncom  3981  iuncom4  3982  iunab  4022  ssiinf  4025  iinab  4037  iunin2  4039  iunun  4054  iunxun  4055  iunxiun  4057  sspwuni  4060  iinpw  4066  cbvdisj  4079  brun  4145  brin  4146  brdif  4147  dftr2  4194  inuni  4250  repizf2lem  4257  unidif0  4263  ssext  4319  pweqb  4321  otth2  4339  opelopabsbALT  4359  eqopab2b  4380  pwin  4385  unisuc  4516  elpwpwel  4578  sucexb  4601  elomssom  4709  xpiundi  4790  xpiundir  4791  poinxp  4801  soinxp  4802  seinxp  4803  inopab  4868  difopab  4869  raliunxp  4877  rexiunxp  4878  iunxpf  4884  cnvco  4921  dmiun  4946  dmuni  4947  dm0rn0  4954  brres  5025  dmres  5040  restidsing  5075  cnvsym  5127  asymref  5129  codir  5132  qfto  5133  cnvopab  5145  cnvdif  5150  rniun  5154  dminss  5158  imainss  5159  cnvcnvsn  5220  resco  5248  imaco  5249  rnco  5250  coiun  5253  coass  5262  ressn  5284  cnviinm  5285  xpcom  5290  funcnv  5398  funcnv3  5399  fncnv  5403  fun11  5404  fnres  5456  dfmpt3  5462  fnopabg  5463  fintm  5530  fin  5531  fores  5578  dff1o3  5598  fun11iun  5613  f11o  5626  f1ompt  5806  fsn  5827  imaiun  5911  isores2  5964  eqoprab2b  6089  opabex3d  6292  opabex3  6293  dfopab2  6361  dfoprab3s  6362  fmpox  6374  tpostpos  6473  dfsmo2  6496  qsid  6812  mapval2  6890  mapsncnv  6907  elixp2  6914  ixpin  6935  xpassen  7057  diffitest  7119  pw1dc0el  7146  supmoti  7235  eqinfti  7262  distrnqg  7650  ltbtwnnq  7679  distrnq0  7722  nqprrnd  7806  ltresr  8102  elznn0nn  9537  xrnemnf  10056  xrnepnf  10057  elioomnf  10247  elxrge0  10257  elfzuzb  10299  fzass4  10342  elfz2nn0  10392  elfzo2  10430  elfzo3  10444  lbfzo0  10465  fzind2  10531  infssuzex  10539  dfrp2  10569  rexfiuz  11612  fisumcom2  12062  prodmodc  12202  fprodcom2fi  12250  4sqlem12  13038  infpn2  13140  xpsfrnel  13490  xpscf  13493  islmod  14370  isbasis2g  14839  tgval2  14845  ntreq0  14926  txuni2  15050  isms2  15248  plyun0  15530  bdceq  16541