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  1937  eeeanv  1989  sbbi  2015  sbco3xzyz  2029  sbcom2v  2041  sbel2x  2054  sb8eu  2095  sb8mo  2096  sb8euh  2105  eu1  2107  cbvmo  2122  mo3h  2136  sbmo  2142  eqcom  2236  abeq1  2344  cbvabw  2359  cbvab  2360  clelab  2362  eqabcb  2371  nfceqi  2382  sbabel  2413  ralbii2  2554  rexbii2  2555  r2alf  2561  r2exf  2562  nfraldya  2579  nfrexdya  2580  r3al  2588  r19.41  2700  r19.42v  2702  ralcomf  2706  rexcomf  2707  reean  2714  3reeanv  2716  rabid2  2723  rabbi  2724  cbvrmow  2729  reubiia  2732  rmobiia  2737  reu5  2764  rmo5  2767  cbvralfw  2769  cbvrexfw  2770  cbvralf  2771  cbvrexf  2772  cbvreuw  2775  cbvreu  2778  cbvrmo  2779  cbvralvw  2784  cbvrexvw  2785  vjust  2816  ceqsex3v  2859  ceqsex4v  2860  ceqsex8v  2862  eueq  2991  reu2  3008  reu6  3009  reu3  3010  rmo4  3013  rmo3f  3017  2rmorex  3026  cbvsbcw  3073  cbvsbc  3074  sbccomlem  3120  rmo3  3138  csbcow  3152  csbabg  3203  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  eqss  3257  uniiunlem  3332  ssequn1  3393  unss  3397  rexun  3403  ralunb  3404  elin3  3414  incom  3415  inass  3435  ssin  3447  ssddif  3459  unssdif  3460  difin  3462  invdif  3467  indif  3468  indi  3472  symdifxor  3491  disj3  3565  eldifpr  3721  rexsns  3733  reusn  3767  prss  3855  tpss  3867  eluni2  3923  elunirab  3932  uniun  3938  uni0b  3944  unissb  3949  elintrab  3966  ssintrab  3977  intun  3985  intpr  3986  iuncom  4002  iuncom4  4003  iunab  4043  ssiinf  4046  iinab  4058  iunin2  4060  iunun  4075  iunxun  4076  iunxiun  4078  sspwuni  4081  iinpw  4087  cbvdisj  4100  brun  4166  brin  4167  brdif  4168  dftr2  4215  inuni  4272  repizf2lem  4279  unidif0  4285  ssext  4342  pweqb  4344  otth2  4362  opelopabsbALT  4382  eqopab2b  4403  pwin  4408  unisuc  4539  elpwpwel  4601  sucexb  4624  elomssom  4732  xpiundi  4813  xpiundir  4814  poinxp  4824  soinxp  4825  seinxp  4826  inopab  4892  difopab  4893  raliunxp  4901  rexiunxp  4902  iunxpf  4908  cnvco  4945  dmiun  4970  dmuni  4971  dm0rn0  4978  brres  5049  dmres  5064  restidsing  5099  cnvsym  5151  asymref  5153  codir  5156  qfto  5157  cnvopab  5169  cnvdif  5174  rniun  5178  dminss  5182  imainss  5183  cnvcnvsn  5244  resco  5272  imaco  5273  rnco  5274  coiun  5277  coass  5286  ressn  5308  cnviinm  5309  xpcom  5314  funcnv  5422  funcnv3  5423  fncnv  5427  fun11  5428  fnres  5480  dfmpt3  5486  fnopabg  5487  fintm  5557  fin  5558  fores  5605  dff1o3  5625  fun11iun  5640  f11o  5653  f1ompt  5833  fsn  5854  imaiun  5939  isores2  5992  eqoprab2b  6119  opabex3d  6323  opabex3  6324  dfopab2  6396  dfoprab3s  6397  fmpox  6409  tpostpos  6508  dfsmo2  6531  qsid  6847  mapval2  6925  mapsncnv  6943  elixp2  6950  ixpin  6971  xpassen  7094  diffitest  7157  pw1dc0el  7184  supmoti  7297  eqinfti  7324  distrnqg  7718  ltbtwnnq  7747  distrnq0  7790  nqprrnd  7874  ltresr  8170  elznn0nn  9608  xrnemnf  10129  xrnepnf  10130  elioomnf  10320  elxrge0  10330  elfzuzb  10372  fzass4  10417  elfz2nn0  10468  elfzo2  10506  elfzo3  10520  lbfzo0  10541  fzind2  10607  infssuzex  10615  dfrp2  10647  rexfiuz  11699  fisumcom2  12149  prodmodc  12289  fprodcom2fi  12337  4sqlem12  13125  ballotfilemelo  13166  ballotfilem2  13172  infpn2  13291  xpsfrnel  13608  xpscf  13611  drngprop  14555  opprdrng  14558  islmod  14565  isbasis2g  15036  tgval2  15042  ntreq0  15123  txuni2  15247  isms2  15445  plyun0  15727  bdceq  16738