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 ⊢ (𝜒 ↔ 𝜃)

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bibi2d  232  pm4.71  393  pm5.32ri  459  mpan10  478  an31  570  an4  592  or4  783  ordir  829  andir  831  3anrot  1014  3orrot  1015  3ancoma  1016  3orcomb  1018  3ioran  1024  3anbi123i  1219  3orbi123i  1220  3or6  1364  xorcom  1437  nfbii  1526  19.26-3an  1536  alnex  1552  19.42h  1739  19.42  1740  equsal  1779  equsalv  1846  sb6  1941  eeeanv  1993  sbbi  2019  sbco3xzyz  2033  sbcom2v  2045  sbel2x  2058  sb8eu  2099  sb8mo  2100  sb8euh  2109  eu1  2111  cbvmo  2126  mo3h  2140  sbmo  2146  eqcom  2240  abeq1  2348  cbvabw  2363  cbvab  2364  clelab  2366  eqabcbw  2376  eqabcb  2377  nfceqi  2388  sbabel  2419  ralbii2  2560  rexbii2  2561  r2alf  2567  r2exf  2568  nfraldya  2585  nfrexdya  2586  r3al  2594  r19.41  2706  r19.42v  2708  ralcomf  2712  rexcomf  2713  reean  2720  3reeanv  2722  rabid2  2729  rabbi  2730  cbvrmow  2735  reubiia  2738  rmobiia  2743  reu5  2770  rmo5  2773  cbvralfw  2775  cbvrexfw  2776  cbvralf  2777  cbvrexf  2778  cbvreuw  2781  cbvreu  2784  cbvrmo  2785  cbvralvw  2790  cbvrexvw  2791  vjust  2822  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  eueq  2997  reu2  3014  reu6  3015  reu3  3016  rmo4  3019  rmo3f  3023  2rmorex  3032  cbvsbcw  3079  cbvsbc  3080  sbccomlem  3126  rmo3  3144  csbcow  3158  csbabg  3209  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  eqss  3263  uniiunlem  3338  ssequn1  3399  unss  3403  rexun  3409  ralunb  3410  elin3  3420  incom  3421  inass  3441  ssin  3453  ssddif  3465  unssdif  3466  difin  3468  invdif  3473  indif  3474  indi  3478  symdifxor  3497  ab0w  3550  disj3  3577  eldifpr  3736  rexsns  3748  reusn  3782  prss  3871  tpss  3883  eluni2  3939  elunirab  3948  uniun  3954  uni0b  3960  unissb  3965  elintrab  3982  ssintrab  3993  intun  4001  intpr  4002  iuncom  4018  iuncom4  4019  iunab  4059  ssiinf  4062  iinab  4074  iunin2  4076  iunun  4091  iunxun  4092  iunxiun  4094  sspwuni  4097  iinpw  4103  cbvdisj  4116  brun  4183  brin  4184  brdif  4185  dftr2  4233  inuni  4293  repizf2lem  4300  unidif0  4306  ssext  4363  pweqb  4365  otth2  4383  opelopabsbALT  4403  eqopab2b  4424  pwin  4429  unisuc  4560  elpwpwel  4623  sucexb  4646  elomssom  4754  xpiundi  4835  xpiundir  4836  poinxp  4846  soinxp  4847  seinxp  4848  inopab  4914  difopab  4915  raliunxp  4923  rexiunxp  4924  iunxpf  4930  cnvco  4967  dmiun  4992  dmuni  4993  dm0rn0  5000  brres  5071  dmres  5086  restidsing  5122  cnvsym  5174  asymref  5176  codir  5179  qfto  5180  cnvopab  5192  cnvdif  5197  rniun  5201  dminss  5205  imainss  5206  cnvcnvsn  5267  resco  5295  imaco  5296  rnco  5297  coiun  5300  coass  5309  ressn  5331  cnviinm  5332  xpcom  5337  funcnv  5445  funcnv3  5446  fncnv  5450  fun11  5451  fnres  5503  dfmpt3  5509  fnopabg  5510  fintm  5580  fin  5581  fores  5628  dff1o3  5648  fun11iun  5663  f11o  5676  f1ompt  5862  fsn  5883  imaiun  5969  isores2  6022  eqoprab2b  6149  opabex3d  6354  opabex3  6355  dfopab2  6427  dfoprab3s  6428  fmpox  6440  tpostpos  6540  dfsmo2  6563  qsid  6879  mapval2  6964  mapsncnv  6983  elixp2  6990  ixpin  7011  xpassen  7134  diffitest  7197  pw1dc0el  7224  supmoti  7339  eqinfti  7366  distrnqg  7760  ltbtwnnq  7789  distrnq0  7832  nqprrnd  7916  ltresr  8212  elznn0nn  9667  xrnemnf  10195  xrnepnf  10196  elioomnf  10386  elxrge0  10396  elfzuzb  10438  fzass4  10484  elfz2nn0  10535  elfzo2  10573  elfzo3  10587  lbfzo0  10608  fzind2  10674  infssuzex  10682  dfrp2  10714  rexfiuz  11776  fisumcom2  12229  prodmodc  12369  fprodcom2fi  12417  4sqlem12  13209  ballotfilemelo  13279  ballotfilem2  13285  infpn2  13404  xpsfrnel  13723  xpscf  13726  drngprop  14725  opprdrng  14728  islmod  14735  isbasis2g  15288  tgval2  15294  ntreq0  15375  txuni2  15499  isms2  15697  plyun0  15979  bdceq  17090  dfrals2  17354  alsbii  17365  ralsbii  17366  cbvals  17370  dfralseu2  17388  alseubii  17397  ralseubii  17398