Theorem sylan9req 2786

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541

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 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722

This theorem is referenced by:  ordintdif  6353  fndmu  6584  fodmrnu  6739  funcoeqres  6790  eqfnun  6965  sspreima  6996  tz7.44-3  8322  fsetfocdm  8780  dfac5lem4  10009  dfac5lem4OLD  10011  zdiv  12535  hashimarni  14340  fprodss  15847  dvdsmulc  16186  smumullem  16395  cncongrcoprm  16573  mgmidmo  18560  reslmhm2b  20981  fclsfnflim  23935  ustuqtop1  24149  ulm2  26314  sineq0  26453  cxple2a  26628  sqff1o  27112  lgsmodeq  27273  eedimeq  28869  frrusgrord0  30310  grpoidinvlem4  30477  hlimuni  31208  dmdsl3  32285  atoml2i  32353  disjpreima  32554  xrge0npcan  32991  poimirlem3  37642  poimirlem4  37643  poimirlem16  37655  poimirlem17  37656  poimirlem19  37658  poimirlem20  37659  poimirlem23  37662  poimirlem24  37663  poimirlem25  37664  poimirlem29  37668  poimirlem31  37670  unidmqs  38671  ltrncnvnid  40145  cdleme20j  40336  cdleme42ke  40503  dia2dimlem13  41094  dvh4dimN  41465  mapdval4N  41650  ccatcan2d  42263  zdivgd  42349  cnreeu  42502  sineq0ALT  44948  cncfiooicc  45911  fourierdlem41  46165  fourierdlem71  46194  bgoldbtbndlem4  47818  bgoldbtbnd  47819  isubgr3stgrlem8  47983  prcof1  49399