Theorem sylan9req 2665

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603

This theorem is referenced by:  ordintdif  5691  fndmu  5906  fodmrnu  6036  funcoeqres  6080  tz7.44-3  7391  dfac5lem4  8832  zdiv  11323  hashimarni  13086  ccatws1lenrev  13260  fprodss  14517  dvdsmulc  14847  smumullem  15052  cncongrcoprm  15222  mgmidmo  17082  reslmhm2b  18875  fclsfnflim  21641  ustuqtop1  21855  ulm2  23943  sineq0  24077  cxple2a  24245  sqff1o  24708  lgsmodeq  24867  eedimeq  25578  grpoidinvlem4  26745  hlimuni  27479  dmdsl3  28558  atoml2i  28626  disjpreima  28779  sspreima  28827  xrge0npcan  29025  poimirlem3  32582  poimirlem4  32583  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem29  32608  poimirlem31  32610  eqfnun  32686  ltrncnvnid  34431  cdleme20j  34624  cdleme42ke  34791  dia2dimlem13  35383  dvh4dimN  35754  mapdval4N  35939  sineq0ALT  38195  cncfiooicc  38780  fourierdlem41  39041  fourierdlem71  39070  bgoldbtbndlem4  40224  bgoldbtbnd  40225