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  431  mpan10  446  an31  486  an4  507  or4  675  ordir  718  andir  720  dcbii  735  3anrot  876  3orrot  877  3ancoma  878  3orcomb  880  3ioran  886  3anbi123i  1077  3orbi123i  1078  3or6  1201  xorcom  1260  nfbii  1338  19.26-3an  1348  alnex  1365  19.42h  1555  19.42  1556  equsal  1593  sb6  1744  eeeanv  1786  sbbi  1811  sbco3xzyz  1825  sbcom2v  1839  sbel2x  1852  sb8eu  1891  sb8mo  1892  sb8euh  1901  eu1  1903  cbvmo  1918  mo3h  1931  sbmo  1937  eqcom  2020  abeq1  2125  cbvab  2138  clelab  2140  nfceqi  2152  sbabel  2181  ralbii2  2308  rexbii2  2309  r2alf  2315  r2exf  2316  nfraldya  2332  nfrexdya  2333  r3al  2340  r19.41  2439  r19.42v  2441  ralcomf  2445  rexcomf  2446  reean  2452  3reeanv  2454  rabid2  2460  rabbi  2461  reubiia  2468  rmobiia  2473  reu5  2496  rmo5  2499  cbvralf  2501  cbvrexf  2502  cbvreu  2505  cbvrmo  2506  vjust  2532  ceqsex3v  2569  ceqsex4v  2570  ceqsex8v  2572  eueq  2685  reu2  2702  reu6  2703  reu3  2704  rmo4  2707  2rmorex  2718  cbvsbc  2764  sbccomlem  2805  rmo3  2822  csbabg  2880  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  eqss  2933  uniiunlem  3001  ssequn1  3086  unss  3090  rexun  3096  ralunb  3097  elin3  3101  incom  3102  inass  3120  ssin  3132  nssinpss  3142  ssddif  3144  unssdif  3145  difin  3147  invdif  3152  indif  3153  indi  3157  symdifxor  3176  disj3  3245  rexsns  3379  reusn  3411  difsnpssim  3477  prss  3490  tpss  3499  eluni2  3554  elunirab  3563  uniun  3569  uni0b  3575  unissb  3580  elintrab  3597  ssintrab  3608  intun  3616  intpr  3617  iuncom  3633  iuncom4  3634  iunab  3673  ssiinf  3676  iinab  3688  iunin2  3690  iunun  3704  iunxun  3705  iunxiun  3706  sspwuni  3709  iinpw  3712  cbvdisj  3725  brun  3780  brin  3781  brdif  3782  dftr2  3826  inuni  3879  repizf2lem  3884  unidif0  3890  ssext  3927  pweqb  3929  otth2  3948  opelopabsbALT  3966  eqopab2b  3986  pwin  3989  unisuc  4095  sucexb  4169  elnn  4251  xpiundi  4321  xpiundir  4322  poinxp  4332  soinxp  4333  seinxp  4334  inopab  4391  difopab  4392  raliunxp  4400  rexiunxp  4401  iunxpf  4407  cnvco  4443  dmiun  4467  dmuni  4468  dm0rn0  4475  brres  4541  dmres  4555  cnvsym  4631  asymref  4633  codir  4636  qfto  4637  cnvopab  4649  cnvdif  4653  rniun  4657  dminss  4661  imainss  4662  cnvcnvsn  4720  resco  4748  imaco  4749  rnco  4750  coiun  4753  coass  4762  ressn  4781  cnviinm  4782  xpcom  4787  funcnv  4882  funcnv3  4883  fncnv  4887  fun11  4888  fnres  4937  dfmpt3  4943  fnopabg  4944  fintm  4996  fin  4997  fores  5036  dff1o3  5053  fun11iun  5068  f11o  5080  f1ompt  5241  fsn  5256  imaiun  5320  isores2  5374  eqoprab2b  5482  opabex3d  5667  opabex3  5668  dfopab2  5734  dfoprab3s  5735  fmpt2x  5745  tpostpos  5797  dfsmo2  5820  qsid  6078  distrnqg  6240  ltbtwnnq  6267  distrnq0  6308  nqprrnd  6392  ltresr  6544  bdceq  7208