Theorem sylan9req 2817

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 2767	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		sylan9req.2	. 2 ⊢ (𝜓 → 𝐵 = 𝐶)
4	2, 3	sylan9eq 2816	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753

This theorem is referenced by:  ordintdif  6412  fndmu  6642  fodmrnu  6800  funcoeqres  6852  eqfnun  7032  sspreima  7063  tz7.44-3  8394  fsetfocdm  8857  dfac5lem4  10109  zdiv  12665  hashimarni  14478  fprodss  16002  dvdsmulc  16340  smumullem  16549  cncongrcoprm  16727  mgmidmo  18717  reslmhm2b  21154  fclsfnflim  24163  ustuqtop1  24377  ulm2  26524  sineq0  26665  cxple2a  26840  sqff1o  27322  lgsmodeq  27482  eedimeq  29214  frrusgrord0  30657  grpoidinvlem4  30825  hlimuni  31556  dmdsl3  32633  atoml2i  32701  disjpreima  32895  xrge0npcan  33306  poimirlem3  38240  poimirlem4  38241  poimirlem16  38253  poimirlem17  38254  poimirlem19  38256  poimirlem20  38257  poimirlem23  38260  poimirlem24  38261  poimirlem25  38262  poimirlem29  38266  poimirlem31  38268  unidmqs  39356  ltrncnvnid  40869  cdleme20j  41060  cdleme42ke  41227  dia2dimlem13  41818  dvh4dimN  42189  mapdval4N  42374  ccatcan2d  42987  zdivgd  43066  cnreeu  43232  sineq0ALT  45615  cncfiooicc  46578  fourierdlem41  46832  fourierdlem71  46861  bgoldbtbndlem4  48540  bgoldbtbnd  48541  isubgr3stgrlem8  48705  prcof1  50133