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  1842  sb6  1936  eeeanv  1987  sbbi  2013  sbco3xzyz  2027  sbcom2v  2039  sbel2x  2052  sb8eu  2093  sb8mo  2094  sb8euh  2103  eu1  2105  cbvmo  2120  mo3h  2134  sbmo  2140  eqcom  2234  abeq1  2342  cbvabw  2357  cbvab  2358  clelab  2360  eqabcb  2369  nfceqi  2380  sbabel  2411  ralbii2  2552  rexbii2  2553  r2alf  2559  r2exf  2560  nfraldya  2577  nfrexdya  2578  r3al  2586  r19.41  2698  r19.42v  2700  ralcomf  2704  rexcomf  2705  reean  2712  3reeanv  2714  rabid2  2721  rabbi  2722  cbvrmow  2727  reubiia  2730  rmobiia  2735  reu5  2762  rmo5  2765  cbvralfw  2767  cbvrexfw  2768  cbvralf  2769  cbvrexf  2770  cbvreuw  2773  cbvreu  2776  cbvrmo  2777  cbvralvw  2782  cbvrexvw  2783  vjust  2814  ceqsex3v  2857  ceqsex4v  2858  ceqsex8v  2860  eueq  2988  reu2  3005  reu6  3006  reu3  3007  rmo4  3010  rmo3f  3014  2rmorex  3023  cbvsbcw  3070  cbvsbc  3071  sbccomlem  3117  rmo3  3135  csbcow  3149  csbabg  3200  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  eqss  3253  uniiunlem  3328  ssequn1  3389  unss  3393  rexun  3399  ralunb  3400  elin3  3410  incom  3411  inass  3431  ssin  3443  ssddif  3455  unssdif  3456  difin  3458  invdif  3463  indif  3464  indi  3468  symdifxor  3487  disj3  3561  eldifpr  3716  rexsns  3728  reusn  3762  prss  3850  tpss  3862  eluni2  3918  elunirab  3927  uniun  3933  uni0b  3939  unissb  3944  elintrab  3961  ssintrab  3972  intun  3980  intpr  3981  iuncom  3997  iuncom4  3998  iunab  4038  ssiinf  4041  iinab  4053  iunin2  4055  iunun  4070  iunxun  4071  iunxiun  4073  sspwuni  4076  iinpw  4082  cbvdisj  4095  brun  4161  brin  4162  brdif  4163  dftr2  4210  inuni  4267  repizf2lem  4274  unidif0  4280  ssext  4337  pweqb  4339  otth2  4357  opelopabsbALT  4377  eqopab2b  4398  pwin  4403  unisuc  4534  elpwpwel  4596  sucexb  4619  elomssom  4727  xpiundi  4808  xpiundir  4809  poinxp  4819  soinxp  4820  seinxp  4821  inopab  4887  difopab  4888  raliunxp  4896  rexiunxp  4897  iunxpf  4903  cnvco  4940  dmiun  4965  dmuni  4966  dm0rn0  4973  brres  5044  dmres  5059  restidsing  5094  cnvsym  5146  asymref  5148  codir  5151  qfto  5152  cnvopab  5164  cnvdif  5169  rniun  5173  dminss  5177  imainss  5178  cnvcnvsn  5239  resco  5267  imaco  5268  rnco  5269  coiun  5272  coass  5281  ressn  5303  cnviinm  5304  xpcom  5309  funcnv  5417  funcnv3  5418  fncnv  5422  fun11  5423  fnres  5475  dfmpt3  5481  fnopabg  5482  fintm  5552  fin  5553  fores  5600  dff1o3  5620  fun11iun  5635  f11o  5648  f1ompt  5828  fsn  5849  imaiun  5933  isores2  5986  eqoprab2b  6111  opabex3d  6314  opabex3  6315  dfopab2  6383  dfoprab3s  6384  fmpox  6396  tpostpos  6495  dfsmo2  6518  qsid  6834  mapval2  6912  mapsncnv  6930  elixp2  6937  ixpin  6958  xpassen  7081  diffitest  7144  pw1dc0el  7171  supmoti  7284  eqinfti  7311  distrnqg  7702  ltbtwnnq  7731  distrnq0  7774  nqprrnd  7858  ltresr  8154  elznn0nn  9591  xrnemnf  10110  xrnepnf  10111  elioomnf  10301  elxrge0  10311  elfzuzb  10353  fzass4  10396  elfz2nn0  10446  elfzo2  10484  elfzo3  10498  lbfzo0  10519  fzind2  10585  infssuzex  10593  dfrp2  10623  rexfiuz  11674  fisumcom2  12124  prodmodc  12264  fprodcom2fi  12312  4sqlem12  13100  ballotfilemelo  13141  ballotfilem2  13142  infpn2  13207  xpsfrnel  13557  xpscf  13560  islmod  14439  isbasis2g  14910  tgval2  14916  ntreq0  14997  txuni2  15121  isms2  15319  plyun0  15601  bdceq  16612