Theorem sylan9req 2785

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  ordintdif  6383  fndmu  6625  fodmrnu  6780  funcoeqres  6831  eqfnun  7009  sspreima  7040  tz7.44-3  8376  fsetfocdm  8834  dfac5lem4  10079  dfac5lem4OLD  10081  zdiv  12604  hashimarni  14406  fprodss  15914  dvdsmulc  16253  smumullem  16462  cncongrcoprm  16640  mgmidmo  18587  reslmhm2b  20961  fclsfnflim  23914  ustuqtop1  24129  ulm2  26294  sineq0  26433  cxple2a  26608  sqff1o  27092  lgsmodeq  27253  eedimeq  28825  frrusgrord0  30269  grpoidinvlem4  30436  hlimuni  31167  dmdsl3  32244  atoml2i  32312  disjpreima  32513  xrge0npcan  32961  poimirlem3  37617  poimirlem4  37618  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem29  37643  poimirlem31  37645  unidmqs  38646  ltrncnvnid  40121  cdleme20j  40312  cdleme42ke  40479  dia2dimlem13  41070  dvh4dimN  41441  mapdval4N  41626  ccatcan2d  42239  zdivgd  42325  cnreeu  42478  sineq0ALT  44926  cncfiooicc  45892  fourierdlem41  46146  fourierdlem71  46175  bgoldbtbndlem4  47809  bgoldbtbnd  47810  isubgr3stgrlem8  47972  prcof1  49377