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  6362  fndmu  6593  fodmrnu  6748  funcoeqres  6799  eqfnun  6975  sspreima  7006  tz7.44-3  8337  fsetfocdm  8795  dfac5lem4  10039  dfac5lem4OLD  10041  zdiv  12564  hashimarni  14366  fprodss  15873  dvdsmulc  16212  smumullem  16421  cncongrcoprm  16599  mgmidmo  18552  reslmhm2b  20976  fclsfnflim  23930  ustuqtop1  24145  ulm2  26310  sineq0  26449  cxple2a  26624  sqff1o  27108  lgsmodeq  27269  eedimeq  28861  frrusgrord0  30302  grpoidinvlem4  30469  hlimuni  31200  dmdsl3  32277  atoml2i  32345  disjpreima  32546  xrge0npcan  32987  poimirlem3  37602  poimirlem4  37603  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem23  37622  poimirlem24  37623  poimirlem25  37624  poimirlem29  37628  poimirlem31  37630  unidmqs  38631  ltrncnvnid  40106  cdleme20j  40297  cdleme42ke  40464  dia2dimlem13  41055  dvh4dimN  41426  mapdval4N  41611  ccatcan2d  42224  zdivgd  42310  cnreeu  42463  sineq0ALT  44910  cncfiooicc  45876  fourierdlem41  46130  fourierdlem71  46159  bgoldbtbndlem4  47793  bgoldbtbnd  47794  isubgr3stgrlem8  47956  prcof1  49361