Theorem sylan9req 2835

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770

This theorem is referenced by:  ordintdif  6025  fndmu  6238  fodmrnu  6374  funcoeqres  6421  tz7.44-3  7787  dfac5lem4  9282  zdiv  11799  hashimarni  13542  fprodss  15081  dvdsmulc  15416  smumullem  15620  cncongrcoprm  15789  mgmidmo  17645  reslmhm2b  19449  fclsfnflim  22239  ustuqtop1  22453  ulm2  24576  sineq0  24711  cxple2a  24882  sqff1o  25360  lgsmodeq  25519  eedimeq  26247  frrusgrord0  27748  grpoidinvlem4  27934  hlimuni  28667  dmdsl3  29746  atoml2i  29814  disjpreima  29960  sspreima  30012  xrge0npcan  30256  poimirlem3  34038  poimirlem4  34039  poimirlem16  34051  poimirlem17  34052  poimirlem19  34054  poimirlem20  34055  poimirlem23  34058  poimirlem24  34059  poimirlem25  34060  poimirlem29  34064  poimirlem31  34066  eqfnun  34141  ltrncnvnid  36281  cdleme20j  36472  cdleme42ke  36639  dia2dimlem13  37230  dvh4dimN  37601  mapdval4N  37786  sineq0ALT  40106  cncfiooicc  41035  fourierdlem41  41292  fourierdlem71  41321  bgoldbtbndlem4  42721  bgoldbtbnd  42722