Theorem sylan9req 2798

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-cleq 2729

This theorem is referenced by:  ordintdif  6355  fndmu  6596  fodmrnu  6751  funcoeqres  6802  sspreima  7005  tz7.44-3  8313  dfac5lem4  9987  zdiv  12495  hashimarni  14260  fprodss  15757  dvdsmulc  16092  smumullem  16298  cncongrcoprm  16472  mgmidmo  18441  reslmhm2b  20421  fclsfnflim  23283  ustuqtop1  23498  ulm2  25649  sineq0  25785  cxple2a  25959  sqff1o  26436  lgsmodeq  26595  eedimeq  27554  frrusgrord0  28991  grpoidinvlem4  29156  hlimuni  29887  dmdsl3  30964  atoml2i  31032  disjpreima  31208  xrge0npcan  31588  poimirlem3  35936  poimirlem4  35937  poimirlem16  35949  poimirlem17  35950  poimirlem19  35952  poimirlem20  35953  poimirlem23  35956  poimirlem24  35957  poimirlem25  35958  poimirlem29  35962  poimirlem31  35964  eqfnun  36036  unidmqs  36972  ltrncnvnid  38446  cdleme20j  38637  cdleme42ke  38804  dia2dimlem13  39395  dvh4dimN  39766  mapdval4N  39951  ccatcan2d  40522  cnreeu  40749  sineq0ALT  42930  cncfiooicc  43823  fourierdlem41  44077  fourierdlem71  44106  bgoldbtbndlem4  45678  bgoldbtbnd  45679