Theorem sylan9req 2793

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  ordintdif  6369  fndmu  6600  fodmrnu  6755  funcoeqres  6806  eqfnun  6984  sspreima  7015  tz7.44-3  8341  fsetfocdm  8802  dfac5lem4  10040  dfac5lem4OLD  10042  zdiv  12566  hashimarni  14368  fprodss  15875  dvdsmulc  16214  smumullem  16423  cncongrcoprm  16601  mgmidmo  18589  reslmhm2b  21010  fclsfnflim  23975  ustuqtop1  24189  ulm2  26354  sineq0  26493  cxple2a  26668  sqff1o  27152  lgsmodeq  27313  eedimeq  28954  frrusgrord0  30398  grpoidinvlem4  30565  hlimuni  31296  dmdsl3  32373  atoml2i  32441  disjpreima  32641  xrge0npcan  33083  poimirlem3  37795  poimirlem4  37796  poimirlem16  37808  poimirlem17  37809  poimirlem19  37811  poimirlem20  37812  poimirlem23  37815  poimirlem24  37816  poimirlem25  37817  poimirlem29  37821  poimirlem31  37823  unidmqs  38911  ltrncnvnid  40424  cdleme20j  40615  cdleme42ke  40782  dia2dimlem13  41373  dvh4dimN  41744  mapdval4N  41929  ccatcan2d  42542  zdivgd  42628  cnreeu  42781  sineq0ALT  45213  cncfiooicc  46174  fourierdlem41  46428  fourierdlem71  46457  bgoldbtbndlem4  48090  bgoldbtbnd  48091  isubgr3stgrlem8  48255  prcof1  49669