Theorem sylan9req 2879

Description: An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)

Hypotheses

Ref	Expression
sylan9req.1	⊢ (𝜑 → 𝐵 = 𝐴)
sylan9req.2	⊢ (𝜓 → 𝐵 = 𝐶)

Assertion

Ref	Expression
sylan9req	⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Proof of Theorem sylan9req

Step	Hyp	Ref	Expression
1		sylan9req.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2829	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		sylan9req.2	. 2 ⊢ (𝜓 → 𝐵 = 𝐶)
4	2, 3	sylan9eq 2878	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  ordintdif  6242  fndmu  6460  fodmrnu  6600  funcoeqres  6647  tz7.44-3  8046  dfac5lem4  9554  zdiv  12055  hashimarni  13805  fprodss  15304  dvdsmulc  15639  smumullem  15843  cncongrcoprm  16016  mgmidmo  17872  reslmhm2b  19828  fclsfnflim  22637  ustuqtop1  22852  ulm2  24975  sineq0  25111  cxple2a  25284  sqff1o  25761  lgsmodeq  25920  eedimeq  26686  frrusgrord0  28121  grpoidinvlem4  28286  hlimuni  29017  dmdsl3  30094  atoml2i  30162  disjpreima  30336  sspreima  30394  xrge0npcan  30683  poimirlem3  34897  poimirlem4  34898  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem29  34923  poimirlem31  34925  eqfnun  34999  unidmqs  35890  ltrncnvnid  37265  cdleme20j  37456  cdleme42ke  37623  dia2dimlem13  38214  dvh4dimN  38585  mapdval4N  38770  ccatcan2d  39134  sineq0ALT  41278  cncfiooicc  42184  fourierdlem41  42440  fourierdlem71  42469  bgoldbtbndlem4  43980  bgoldbtbnd  43981