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  498  an4  520  or4  687  ordir  729  andir  731  dcbii  746  3anrot  889  3orrot  890  3ancoma  891  3orcomb  893  3ioran  899  3anbi123i  1092  3orbi123i  1093  3or6  1217  xorcom  1276  nfbii  1359  19.26-3an  1369  alnex  1385  19.42h  1574  19.42  1575  equsal  1612  sb6  1763  eeeanv  1805  sbbi  1830  sbco3xzyz  1844  sbcom2v  1858  sbel2x  1871  sb8eu  1910  sb8mo  1911  sb8euh  1920  eu1  1922  cbvmo  1937  mo3h  1950  sbmo  1956  eqcom  2039  abeq1  2144  cbvab  2157  clelab  2159  nfceqi  2171  sbabel  2200  ralbii2  2328  rexbii2  2329  r2alf  2335  r2exf  2336  nfraldya  2352  nfrexdya  2353  r3al  2360  r19.41  2459  r19.42v  2461  ralcomf  2465  rexcomf  2466  reean  2472  3reeanv  2474  rabid2  2480  rabbi  2481  reubiia  2488  rmobiia  2493  reu5  2516  rmo5  2519  cbvralf  2521  cbvrexf  2522  cbvreu  2525  cbvrmo  2526  vjust  2552  ceqsex3v  2590  ceqsex4v  2591  ceqsex8v  2593  eueq  2706  reu2  2723  reu6  2724  reu3  2725  rmo4  2728  2rmorex  2739  cbvsbc  2785  sbccomlem  2826  rmo3  2843  csbabg  2901  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  eqss  2954  uniiunlem  3022  ssequn1  3107  unss  3111  rexun  3117  ralunb  3118  elin3  3122  incom  3123  inass  3141  ssin  3153  nssinpss  3163  ssddif  3165  unssdif  3166  difin  3168  invdif  3173  indif  3174  indi  3178  symdifxor  3197  disj3  3266  rexsns  3400  reusn  3432  difsnpssim  3498  prss  3511  tpss  3520  eluni2  3575  elunirab  3584  uniun  3590  uni0b  3596  unissb  3601  elintrab  3618  ssintrab  3629  intun  3637  intpr  3638  iuncom  3654  iuncom4  3655  iunab  3694  ssiinf  3697  iinab  3709  iunin2  3711  iunun  3725  iunxun  3726  iunxiun  3727  sspwuni  3730  iinpw  3733  cbvdisj  3746  brun  3801  brin  3802  brdif  3803  dftr2  3847  inuni  3900  repizf2lem  3905  unidif0  3911  ssext  3948  pweqb  3950  otth2  3969  opelopabsbALT  3987  eqopab2b  4007  pwin  4010  unisuc  4116  sucexb  4189  elnn  4271  xpiundi  4341  xpiundir  4342  poinxp  4352  soinxp  4353  seinxp  4354  inopab  4411  difopab  4412  raliunxp  4420  rexiunxp  4421  iunxpf  4427  cnvco  4463  dmiun  4487  dmuni  4488  dm0rn0  4495  brres  4561  dmres  4575  cnvsym  4651  asymref  4653  codir  4656  qfto  4657  cnvopab  4669  cnvdif  4673  rniun  4677  dminss  4681  imainss  4682  cnvcnvsn  4740  resco  4768  imaco  4769  rnco  4770  coiun  4773  coass  4782  ressn  4801  cnviinm  4802  xpcom  4807  funcnv  4903  funcnv3  4904  fncnv  4908  fun11  4909  fnres  4958  dfmpt3  4964  fnopabg  4965  fintm  5018  fin  5019  fores  5058  dff1o3  5075  fun11iun  5090  f11o  5102  f1ompt  5263  fsn  5278  imaiun  5342  isores2  5396  eqoprab2b  5505  opabex3d  5690  opabex3  5691  dfopab2  5757  dfoprab3s  5758  fmpt2x  5768  tpostpos  5820  dfsmo2  5843  qsid  6107  xpassen  6240  distrnqg  6371  ltbtwnnq  6399  distrnq0  6442  nqprrnd  6526  ltresr  6736  elznn0nn  8035  xrnemnf  8469  xrnepnf  8470  elioomnf  8607  elxrge0  8617  elfzuzb  8654  fzass4  8695  elfz2nn0  8743  elfzo2  8777  elfzo3  8789  lbfzo0  8807  fzind2  8865  bdceq  9297