Theorem sylan9req 2800

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  ordintdif  6300  fndmu  6524  fodmrnu  6680  funcoeqres  6730  sspreima  6927  tz7.44-3  8210  dfac5lem4  9813  zdiv  12320  hashimarni  14084  fprodss  15586  dvdsmulc  15921  smumullem  16127  cncongrcoprm  16303  mgmidmo  18259  reslmhm2b  20231  fclsfnflim  23086  ustuqtop1  23301  ulm2  25449  sineq0  25585  cxple2a  25759  sqff1o  26236  lgsmodeq  26395  eedimeq  27169  frrusgrord0  28605  grpoidinvlem4  28770  hlimuni  29501  dmdsl3  30578  atoml2i  30646  disjpreima  30824  xrge0npcan  31205  poimirlem3  35707  poimirlem4  35708  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem29  35733  poimirlem31  35735  eqfnun  35807  unidmqs  36693  ltrncnvnid  38068  cdleme20j  38259  cdleme42ke  38426  dia2dimlem13  39017  dvh4dimN  39388  mapdval4N  39573  ccatcan2d  40145  cnreeu  40359  sineq0ALT  42446  cncfiooicc  43325  fourierdlem41  43579  fourierdlem71  43608  bgoldbtbndlem4  45148  bgoldbtbnd  45149