Theorem sylan9req 2818

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754

This theorem is used by:  ordintdif  6413  fndmu  6643  fodmrnu  6801  funcoeqres  6853  eqfnun  7033  sspreima  7064  tz7.44-3  8401  fsetfocdm  8866  dfac5lem4  10133  zdiv  12695  hashimarni  14510  fprodss  16041  dvdsmulc  16379  smumullem  16588  cncongrcoprm  16766  mgmidmo  18758  reslmhm2b  21244  fclsfnflim  24259  ustuqtop1  24473  ulm2  26628  sineq0  26769  cxple2a  26944  sqff1o  27426  lgsmodeq  27586  eedimeq  29363  frrusgrord0  30828  grpoidinvlem4  30996  hlimuni  31727  dmdsl3  32804  atoml2i  32872  disjpreima  33065  xrge0npcan  33468  poimirlem3  38380  poimirlem4  38381  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem29  38406  poimirlem31  38408  unidmqs  39495  ltrncnvnid  41008  cdleme20j  41199  cdleme42ke  41366  dia2dimlem13  41957  dvh4dimN  42328  mapdval4N  42513  ccatcan2d  43126  zdivgd  43220  cnreeu  43386  sineq0ALT  45767  cncfiooicc  46730  fourierdlem41  46984  fourierdlem71  47013  bgoldbtbndlem4  48732  bgoldbtbnd  48733  isubgr3stgrlem8  48897  prcof1  50322