Theorem sylan9req 2812

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-cleq 2748

This theorem is referenced by:  ordintdif  6386  fndmu  6617  fodmrnu  6775  funcoeqres  6827  eqfnun  7007  sspreima  7038  tz7.44-3  8367  fsetfocdm  8831  dfac5lem4  10072  dfac5lem4OLD  10074  zdiv  12633  hashimarni  14444  fprodss  15954  dvdsmulc  16293  smumullem  16502  cncongrcoprm  16680  mgmidmo  18670  reslmhm2b  21094  fclsfnflim  24060  ustuqtop1  24274  ulm2  26418  sineq0  26559  cxple2a  26734  sqff1o  27216  lgsmodeq  27376  eedimeq  29038  frrusgrord0  30481  grpoidinvlem4  30649  hlimuni  31380  dmdsl3  32457  atoml2i  32525  disjpreima  32726  xrge0npcan  33152  poimirlem3  38070  poimirlem4  38071  poimirlem16  38083  poimirlem17  38084  poimirlem19  38086  poimirlem20  38087  poimirlem23  38090  poimirlem24  38091  poimirlem25  38092  poimirlem29  38096  poimirlem31  38098  unidmqs  39186  ltrncnvnid  40699  cdleme20j  40890  cdleme42ke  41057  dia2dimlem13  41648  dvh4dimN  42019  mapdval4N  42204  ccatcan2d  42815  zdivgd  42894  cnreeu  43060  sineq0ALT  45460  cncfiooicc  46416  fourierdlem41  46670  fourierdlem71  46699  bgoldbtbndlem4  48378  bgoldbtbnd  48379  isubgr3stgrlem8  48543  prcof1  49957