Theorem sylan9req 2816

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  ordintdif  6414  fndmu  6646  fodmrnu  6804  funcoeqres  6856  eqfnun  7036  sspreima  7067  tz7.44-3  8417  fsetfocdm  8884  dfac5lem4  10206  zdiv  12770  hashimarni  14587  fprodss  16116  dvdsmulc  16454  smumullem  16663  cncongrcoprm  16846  mgmidmo  18839  reslmhm2b  21330  fclsfnflim  24347  ustuqtop1  24561  ulm2  26713  sineq0  26853  cxple2a  27028  sqff1o  27510  lgsmodeq  27670  eedimeq  29477  frrusgrord0  30942  grpoidinvlem4  31110  hlimuni  31841  dmdsl3  32918  atoml2i  32986  disjpreima  33221  xrge0npcan  33624  poimirlem3  38617  poimirlem4  38618  poimirlem16  38630  poimirlem17  38631  poimirlem19  38633  poimirlem20  38634  poimirlem23  38637  poimirlem24  38638  poimirlem25  38639  poimirlem29  38643  poimirlem31  38645  unidmqs  39747  ltrncnvnid  41260  cdleme20j  41451  cdleme42ke  41618  dia2dimlem13  42209  dvh4dimN  42580  mapdval4N  42765  ccatcan2d  43378  zdivgd  43464  cnreeu  43630  sineq0ALT  45995  cncfiooicc  46980  fourierdlem41  47234  fourierdlem71  47263  bgoldbtbndlem4  48982  bgoldbtbnd  48983  isubgr3stgrlem8  49147  prcof1  50572