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  3824  tpss  3836  eluni2  3892  elunirab  3901  uniun  3907  uni0b  3913  unissb  3918  elintrab  3935  ssintrab  3946  intun  3954  intpr  3955  iuncom  3971  iuncom4  3972  iunab  4012  ssiinf  4015  iinab  4027  iunin2  4029  iunun  4044  iunxun  4045  iunxiun  4047  sspwuni  4050  iinpw  4056  cbvdisj  4069  brun  4135  brin  4136  brdif  4137  dftr2  4184  inuni  4239  repizf2lem  4245  unidif0  4251  ssext  4307  pweqb  4309  otth2  4327  opelopabsbALT  4347  eqopab2b  4368  pwin  4373  unisuc  4504  elpwpwel  4566  sucexb  4589  elomssom  4697  xpiundi  4777  xpiundir  4778  poinxp  4788  soinxp  4789  seinxp  4790  inopab  4854  difopab  4855  raliunxp  4863  rexiunxp  4864  iunxpf  4870  cnvco  4907  dmiun  4932  dmuni  4933  dm0rn0  4940  brres  5011  dmres  5026  restidsing  5061  cnvsym  5112  asymref  5114  codir  5117  qfto  5118  cnvopab  5130  cnvdif  5135  rniun  5139  dminss  5143  imainss  5144  cnvcnvsn  5205  resco  5233  imaco  5234  rnco  5235  coiun  5238  coass  5247  ressn  5269  cnviinm  5270  xpcom  5275  funcnv  5382  funcnv3  5383  fncnv  5387  fun11  5388  fnres  5440  dfmpt3  5446  fnopabg  5447  fintm  5513  fin  5514  fores  5560  dff1o3  5580  fun11iun  5595  f11o  5607  f1ompt  5788  fsn  5809  imaiun  5890  isores2  5943  eqoprab2b  6068  opabex3d  6272  opabex3  6273  dfopab2  6341  dfoprab3s  6342  fmpox  6352  tpostpos  6416  dfsmo2  6439  qsid  6755  mapval2  6833  mapsncnv  6850  elixp2  6857  ixpin  6878  xpassen  6997  diffitest  7057  pw1dc0el  7084  supmoti  7171  eqinfti  7198  distrnqg  7585  ltbtwnnq  7614  distrnq0  7657  nqprrnd  7741  ltresr  8037  elznn0nn  9471  xrnemnf  9985  xrnepnf  9986  elioomnf  10176  elxrge0  10186  elfzuzb  10227  fzass4  10270  elfz2nn0  10320  elfzo2  10358  elfzo3  10372  lbfzo0  10393  fzind2  10457  infssuzex  10465  dfrp2  10495  rexfiuz  11515  fisumcom2  11964  prodmodc  12104  fprodcom2fi  12152  4sqlem12  12940  infpn2  13042  xpsfrnel  13392  xpscf  13395  islmod  14270  isbasis2g  14734  tgval2  14740  ntreq0  14821  txuni2  14945  isms2  15143  plyun0  15425  bdceq  16260