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  778  ordir  824  andir  826  3anrot  1009  3orrot  1010  3ancoma  1011  3orcomb  1013  3ioran  1019  3anbi123i  1214  3orbi123i  1215  3or6  1359  xorcom  1432  nfbii  1521  19.26-3an  1531  alnex  1547  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  2354  cbvab  2355  clelab  2357  nfceqi  2370  sbabel  2401  ralbii2  2542  rexbii2  2543  r2alf  2549  r2exf  2550  nfraldya  2567  nfrexdya  2568  r3al  2576  r19.41  2688  r19.42v  2690  ralcomf  2694  rexcomf  2695  reean  2702  3reeanv  2704  rabid2  2710  rabbi  2711  cbvrmow  2716  reubiia  2719  rmobiia  2724  reu5  2751  rmo5  2754  cbvralfw  2756  cbvrexfw  2757  cbvralf  2758  cbvrexf  2759  cbvreuw  2762  cbvreu  2765  cbvrmo  2766  cbvralvw  2771  cbvrexvw  2772  vjust  2803  ceqsex3v  2846  ceqsex4v  2847  ceqsex8v  2849  eueq  2977  reu2  2994  reu6  2995  reu3  2996  rmo4  2999  rmo3f  3003  2rmorex  3012  cbvsbcw  3059  cbvsbc  3060  sbccomlem  3106  rmo3  3124  csbcow  3138  csbabg  3189  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  eqss  3242  uniiunlem  3316  ssequn1  3377  unss  3381  rexun  3387  ralunb  3388  elin3  3398  incom  3399  inass  3417  ssin  3429  ssddif  3441  unssdif  3442  difin  3444  invdif  3449  indif  3450  indi  3454  symdifxor  3473  disj3  3547  eldifpr  3696  rexsns  3708  reusn  3742  prss  3829  tpss  3841  eluni2  3897  elunirab  3906  uniun  3912  uni0b  3918  unissb  3923  elintrab  3940  ssintrab  3951  intun  3959  intpr  3960  iuncom  3976  iuncom4  3977  iunab  4017  ssiinf  4020  iinab  4032  iunin2  4034  iunun  4049  iunxun  4050  iunxiun  4052  sspwuni  4055  iinpw  4061  cbvdisj  4074  brun  4140  brin  4141  brdif  4142  dftr2  4189  inuni  4245  repizf2lem  4251  unidif0  4257  ssext  4313  pweqb  4315  otth2  4333  opelopabsbALT  4353  eqopab2b  4374  pwin  4379  unisuc  4510  elpwpwel  4572  sucexb  4595  elomssom  4703  xpiundi  4784  xpiundir  4785  poinxp  4795  soinxp  4796  seinxp  4797  inopab  4862  difopab  4863  raliunxp  4871  rexiunxp  4872  iunxpf  4878  cnvco  4915  dmiun  4940  dmuni  4941  dm0rn0  4948  brres  5019  dmres  5034  restidsing  5069  cnvsym  5120  asymref  5122  codir  5125  qfto  5126  cnvopab  5138  cnvdif  5143  rniun  5147  dminss  5151  imainss  5152  cnvcnvsn  5213  resco  5241  imaco  5242  rnco  5243  coiun  5246  coass  5255  ressn  5277  cnviinm  5278  xpcom  5283  funcnv  5391  funcnv3  5392  fncnv  5396  fun11  5397  fnres  5449  dfmpt3  5455  fnopabg  5456  fintm  5522  fin  5523  fores  5569  dff1o3  5589  fun11iun  5604  f11o  5617  f1ompt  5798  fsn  5819  imaiun  5900  isores2  5953  eqoprab2b  6078  opabex3d  6282  opabex3  6283  dfopab2  6351  dfoprab3s  6352  fmpox  6364  tpostpos  6429  dfsmo2  6452  qsid  6768  mapval2  6846  mapsncnv  6863  elixp2  6870  ixpin  6891  xpassen  7013  diffitest  7075  pw1dc0el  7102  supmoti  7191  eqinfti  7218  distrnqg  7606  ltbtwnnq  7635  distrnq0  7678  nqprrnd  7762  ltresr  8058  elznn0nn  9492  xrnemnf  10011  xrnepnf  10012  elioomnf  10202  elxrge0  10212  elfzuzb  10253  fzass4  10296  elfz2nn0  10346  elfzo2  10384  elfzo3  10398  lbfzo0  10419  fzind2  10484  infssuzex  10492  dfrp2  10522  rexfiuz  11549  fisumcom2  11998  prodmodc  12138  fprodcom2fi  12186  4sqlem12  12974  infpn2  13076  xpsfrnel  13426  xpscf  13429  islmod  14304  isbasis2g  14768  tgval2  14774  ntreq0  14855  txuni2  14979  isms2  15177  plyun0  15459  bdceq  16437