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  2800  ceqsex3v  2843  ceqsex4v  2844  ceqsex8v  2846  eueq  2974  reu2  2991  reu6  2992  reu3  2993  rmo4  2996  rmo3f  3000  2rmorex  3009  cbvsbcw  3056  cbvsbc  3057  sbccomlem  3103  rmo3  3121  csbcow  3135  csbabg  3186  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  eqss  3239  uniiunlem  3313  ssequn1  3374  unss  3378  rexun  3384  ralunb  3385  elin3  3395  incom  3396  inass  3414  ssin  3426  ssddif  3438  unssdif  3439  difin  3441  invdif  3446  indif  3447  indi  3451  symdifxor  3470  disj3  3544  eldifpr  3693  rexsns  3705  reusn  3737  prss  3823  tpss  3835  eluni2  3891  elunirab  3900  uniun  3906  uni0b  3912  unissb  3917  elintrab  3934  ssintrab  3945  intun  3953  intpr  3954  iuncom  3970  iuncom4  3971  iunab  4011  ssiinf  4014  iinab  4026  iunin2  4028  iunun  4043  iunxun  4044  iunxiun  4046  sspwuni  4049  iinpw  4055  cbvdisj  4068  brun  4134  brin  4135  brdif  4136  dftr2  4183  inuni  4238  repizf2lem  4244  unidif0  4250  ssext  4306  pweqb  4308  otth2  4326  opelopabsbALT  4346  eqopab2b  4367  pwin  4372  unisuc  4503  elpwpwel  4565  sucexb  4588  elomssom  4696  xpiundi  4776  xpiundir  4777  poinxp  4787  soinxp  4788  seinxp  4789  inopab  4853  difopab  4854  raliunxp  4862  rexiunxp  4863  iunxpf  4869  cnvco  4906  dmiun  4931  dmuni  4932  dm0rn0  4939  brres  5010  dmres  5025  restidsing  5060  cnvsym  5111  asymref  5113  codir  5116  qfto  5117  cnvopab  5129  cnvdif  5134  rniun  5138  dminss  5142  imainss  5143  cnvcnvsn  5204  resco  5232  imaco  5233  rnco  5234  coiun  5237  coass  5246  ressn  5268  cnviinm  5269  xpcom  5274  funcnv  5381  funcnv3  5382  fncnv  5386  fun11  5387  fnres  5439  dfmpt3  5445  fnopabg  5446  fintm  5510  fin  5511  fores  5557  dff1o3  5577  fun11iun  5592  f11o  5604  f1ompt  5785  fsn  5806  imaiun  5883  isores2  5936  eqoprab2b  6061  opabex3d  6264  opabex3  6265  dfopab2  6333  dfoprab3s  6334  fmpox  6344  tpostpos  6408  dfsmo2  6431  qsid  6745  mapval2  6823  mapsncnv  6840  elixp2  6847  ixpin  6868  xpassen  6985  diffitest  7045  pw1dc0el  7069  supmoti  7156  eqinfti  7183  distrnqg  7570  ltbtwnnq  7599  distrnq0  7642  nqprrnd  7726  ltresr  8022  elznn0nn  9456  xrnemnf  9969  xrnepnf  9970  elioomnf  10160  elxrge0  10170  elfzuzb  10211  fzass4  10254  elfz2nn0  10304  elfzo2  10342  elfzo3  10356  lbfzo0  10377  fzind2  10440  infssuzex  10448  dfrp2  10478  rexfiuz  11495  fisumcom2  11944  prodmodc  12084  fprodcom2fi  12132  4sqlem12  12920  infpn2  13022  xpsfrnel  13372  xpscf  13375  islmod  14249  isbasis2g  14713  tgval2  14719  ntreq0  14800  txuni2  14924  isms2  15122  plyun0  15404  bdceq  16163