Theorem sylan9req 2792

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

Syntax hints:   → wi 4   ∧ wa 396   = 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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  ordintdif  6372  fndmu  6614  fodmrnu  6769  funcoeqres  6820  sspreima  7023  tz7.44-3  8359  dfac5lem4  10071  zdiv  12582  hashimarni  14351  fprodss  15842  dvdsmulc  16177  smumullem  16383  cncongrcoprm  16557  mgmidmo  18529  reslmhm2b  20572  fclsfnflim  23415  ustuqtop1  23630  ulm2  25781  sineq0  25917  cxple2a  26091  sqff1o  26568  lgsmodeq  26727  eedimeq  27910  frrusgrord0  29347  grpoidinvlem4  29512  hlimuni  30243  dmdsl3  31320  atoml2i  31388  disjpreima  31569  xrge0npcan  31955  poimirlem3  36154  poimirlem4  36155  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem23  36174  poimirlem24  36175  poimirlem25  36176  poimirlem29  36180  poimirlem31  36182  eqfnun  36254  unidmqs  37189  ltrncnvnid  38663  cdleme20j  38854  cdleme42ke  39021  dia2dimlem13  39612  dvh4dimN  39983  mapdval4N  40168  ccatcan2d  40738  cnreeu  40995  sineq0ALT  43341  cncfiooicc  44255  fourierdlem41  44509  fourierdlem71  44538  bgoldbtbndlem4  46120  bgoldbtbnd  46121