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 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 2702

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

This theorem is referenced by:  ordintdif  6386  fndmu  6628  fodmrnu  6783  funcoeqres  6834  eqfnun  7012  sspreima  7043  tz7.44-3  8379  fsetfocdm  8837  dfac5lem4  10086  dfac5lem4OLD  10088  zdiv  12611  hashimarni  14413  fprodss  15921  dvdsmulc  16260  smumullem  16469  cncongrcoprm  16647  mgmidmo  18594  reslmhm2b  20968  fclsfnflim  23921  ustuqtop1  24136  ulm2  26301  sineq0  26440  cxple2a  26615  sqff1o  27099  lgsmodeq  27260  eedimeq  28832  frrusgrord0  30276  grpoidinvlem4  30443  hlimuni  31174  dmdsl3  32251  atoml2i  32319  disjpreima  32520  xrge0npcan  32968  poimirlem3  37624  poimirlem4  37625  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem29  37650  poimirlem31  37652  unidmqs  38653  ltrncnvnid  40128  cdleme20j  40319  cdleme42ke  40486  dia2dimlem13  41077  dvh4dimN  41448  mapdval4N  41633  ccatcan2d  42246  zdivgd  42332  cnreeu  42485  sineq0ALT  44933  cncfiooicc  45899  fourierdlem41  46153  fourierdlem71  46182  bgoldbtbndlem4  47813  bgoldbtbnd  47814  isubgr3stgrlem8  47976  prcof1  49381