Theorem sylan9req 2677

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  ordintdif  5774  fndmu  5992  fodmrnu  6123  funcoeqres  6167  tz7.44-3  7504  dfac5lem4  8949  zdiv  11447  hashimarni  13228  ccatws1lenrevOLD  13408  fprodss  14678  dvdsmulc  15009  smumullem  15214  cncongrcoprm  15384  mgmidmo  17259  reslmhm2b  19054  fclsfnflim  21831  ustuqtop1  22045  ulm2  24139  sineq0  24273  cxple2a  24445  sqff1o  24908  lgsmodeq  25067  eedimeq  25778  frrusgrord0  27204  grpoidinvlem4  27361  hlimuni  28095  dmdsl3  29174  atoml2i  29242  disjpreima  29397  sspreima  29447  xrge0npcan  29694  poimirlem3  33412  poimirlem4  33413  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem29  33438  poimirlem31  33440  eqfnun  33516  ltrncnvnid  35413  cdleme20j  35606  cdleme42ke  35773  dia2dimlem13  36365  dvh4dimN  36736  mapdval4N  36921  sineq0ALT  39173  cncfiooicc  40107  fourierdlem41  40365  fourierdlem71  40394  bgoldbtbndlem4  41696  bgoldbtbnd  41697