Theorem sylan9req 2791

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 2790	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

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

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  ordintdif  6413  fndmu  6655  fodmrnu  6812  funcoeqres  6863  eqfnun  7037  sspreima  7068  tz7.44-3  8410  dfac5lem4  10123  zdiv  12636  hashimarni  14405  fprodss  15896  dvdsmulc  16231  smumullem  16437  cncongrcoprm  16611  mgmidmo  18585  reslmhm2b  20809  fclsfnflim  23751  ustuqtop1  23966  ulm2  26133  sineq0  26269  cxple2a  26443  sqff1o  26922  lgsmodeq  27081  eedimeq  28423  frrusgrord0  29860  grpoidinvlem4  30027  hlimuni  30758  dmdsl3  31835  atoml2i  31903  disjpreima  32082  xrge0npcan  32462  poimirlem3  36794  poimirlem4  36795  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem23  36814  poimirlem24  36815  poimirlem25  36816  poimirlem29  36820  poimirlem31  36822  unidmqs  37827  ltrncnvnid  39301  cdleme20j  39492  cdleme42ke  39659  dia2dimlem13  40250  dvh4dimN  40621  mapdval4N  40806  ccatcan2d  41375  cnreeu  41643  sineq0ALT  44000  cncfiooicc  44908  fourierdlem41  45162  fourierdlem71  45191  bgoldbtbndlem4  46774  bgoldbtbnd  46775