Theorem 3bitr4i 201

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 176	. 2 ⊢ (φ ↔ θ)
5	1, 4	bitri 173	1 ⊢ (χ ↔ θ)

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bibi2d  221  pm4.71  369  pm5.32ri  428  mpan10  443  an31  483  an4  505  or4  672  ordir  714  andir  716  dcbii  731  3anrot  872  3orrot  873  3ancoma  874  3orcomb  876  3ioran  882  3anbi123i  1074  3orbi123i  1075  3or6  1199  xorcom  1258  nfbii  1336  19.26-3an  1346  alnex  1362  19.42h  1551  19.42  1552  equsal  1589  sb6  1740  eeeanv  1782  sbbi  1807  sbco3xzyz  1821  sbcom2v  1835  sbel2x  1848  sb8eu  1887  sb8mo  1888  sb8euh  1897  eu1  1899  cbvmo  1914  mo3h  1927  sbmo  1933  eqcom  2016  abeq1  2121  cbvab  2134  clelab  2136  nfceqi  2148  sbabel  2177  ralbii2  2304  rexbii2  2305  r2alf  2311  r2exf  2312  nfraldya  2328  nfrexdya  2329  r3al  2336  r19.41  2435  r19.42v  2437  ralcomf  2441  rexcomf  2442  reean  2448  3reeanv  2450  rabid2  2456  rabbi  2457  reubiia  2464  rmobiia  2469  reu5  2492  rmo5  2495  cbvralf  2497  cbvrexf  2498  cbvreu  2501  cbvrmo  2502  vjust  2528  ceqsex3v  2565  ceqsex4v  2566  ceqsex8v  2568  eueq  2681  reu2  2698  reu6  2699  reu3  2700  rmo4  2703  2rmorex  2714  cbvsbc  2760  sbccomlem  2801  rmo3  2818  csbabg  2876  cbvralcsf  2877  cbvrexcsf  2878  cbvreucsf  2879  eqss  2929  uniiunlem  2997  ssequn1  3082  unss  3086  rexun  3092  ralunb  3093  elin3  3097  incom  3098  inass  3116  ssin  3128  nssinpss  3138  ssddif  3140  unssdif  3141  difin  3143  invdif  3148  indif  3149  indi  3153  symdifxor  3172  disj3  3241  rexsns  3373  reusn  3405  difsnpssim  3471  prss  3484  tpss  3493  eluni2  3548  elunirab  3557  uniun  3563  uni0b  3569  unissb  3574  elintrab  3591  ssintrab  3602  intun  3610  intpr  3611  iuncom  3627  iuncom4  3628  iunab  3667  ssiinf  3670  iinab  3682  iunin2  3684  iunun  3698  iunxun  3699  iunxiun  3700  sspwuni  3703  iinpw  3706  cbvdisj  3719  brun  3774  brin  3775  brdif  3776  dftr2  3820  inuni  3873  repizf2lem  3878  unidif0  3884  ssext  3921  pweqb  3923  otth2  3942  opelopabsbALT  3960  eqopab2b  3980  pwin  3983  unisuc  4089  sucexb  4162  elnn  4244  xpiundi  4314  xpiundir  4315  poinxp  4325  soinxp  4326  seinxp  4327  inopab  4384  difopab  4385  raliunxp  4393  rexiunxp  4394  iunxpf  4400  cnvco  4436  dmiun  4460  dmuni  4461  dm0rn0  4468  brres  4534  dmres  4548  cnvsym  4624  asymref  4626  codir  4629  qfto  4630  cnvopab  4642  cnvdif  4646  rniun  4650  dminss  4654  imainss  4655  cnvcnvsn  4713  resco  4741  imaco  4742  rnco  4743  coiun  4746  coass  4755  ressn  4774  cnviinm  4775  xpcom  4780  funcnv  4875  funcnv3  4876  fncnv  4880  fun11  4881  fnres  4930  dfmpt3  4936  fnopabg  4937  fintm  4989  fin  4990  fores  5029  dff1o3  5046  fun11iun  5061  f11o  5073  f1ompt  5234  fsn  5249  imaiun  5313  isores2  5367  eqoprab2b  5475  opabex3d  5660  opabex3  5661  dfopab2  5727  dfoprab3s  5728  fmpt2x  5738  tpostpos  5790  dfsmo2  5813  qsid  6071  distrnqg  6233  ltbtwnnq  6260  distrnq0  6301  nqprrnd  6385  ltresr  6546  elznn0nn  7834  xrnemnf  8176  xrnepnf  8177  bdceq  8299