Theorem sylan9req 2789

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 2739	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		sylan9req.2	. 2 ⊢ (𝜓 → 𝐵 = 𝐶)
4	2, 3	sylan9eq 2788	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 2123  ax-ext 2705

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

This theorem is referenced by:  ordintdif  6365  fndmu  6596  fodmrnu  6751  funcoeqres  6802  eqfnun  6979  sspreima  7010  tz7.44-3  8336  fsetfocdm  8794  dfac5lem4  10027  dfac5lem4OLD  10029  zdiv  12553  hashimarni  14358  fprodss  15865  dvdsmulc  16204  smumullem  16413  cncongrcoprm  16591  mgmidmo  18578  reslmhm2b  20998  fclsfnflim  23952  ustuqtop1  24166  ulm2  26331  sineq0  26470  cxple2a  26645  sqff1o  27129  lgsmodeq  27290  eedimeq  28887  frrusgrord0  30331  grpoidinvlem4  30498  hlimuni  31229  dmdsl3  32306  atoml2i  32374  disjpreima  32575  xrge0npcan  33012  poimirlem3  37673  poimirlem4  37674  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem23  37693  poimirlem24  37694  poimirlem25  37695  poimirlem29  37699  poimirlem31  37701  unidmqs  38762  ltrncnvnid  40236  cdleme20j  40427  cdleme42ke  40594  dia2dimlem13  41185  dvh4dimN  41556  mapdval4N  41741  ccatcan2d  42359  zdivgd  42445  cnreeu  42598  sineq0ALT  45043  cncfiooicc  46006  fourierdlem41  46260  fourierdlem71  46289  bgoldbtbndlem4  47922  bgoldbtbnd  47923  isubgr3stgrlem8  48087  prcof1  49503