Theorem sylan9req 2796

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  ordintdif  6436  fndmu  6676  fodmrnu  6829  funcoeqres  6880  eqfnun  7057  sspreima  7088  tz7.44-3  8447  fsetfocdm  8900  dfac5lem4  10164  dfac5lem4OLD  10166  zdiv  12686  hashimarni  14477  fprodss  15981  dvdsmulc  16318  smumullem  16526  cncongrcoprm  16704  mgmidmo  18686  reslmhm2b  21071  fclsfnflim  24051  ustuqtop1  24266  ulm2  26443  sineq0  26581  cxple2a  26756  sqff1o  27240  lgsmodeq  27401  eedimeq  28928  frrusgrord0  30369  grpoidinvlem4  30536  hlimuni  31267  dmdsl3  32344  atoml2i  32412  disjpreima  32604  xrge0npcan  33008  poimirlem3  37610  poimirlem4  37611  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem29  37636  poimirlem31  37638  unidmqs  38636  ltrncnvnid  40110  cdleme20j  40301  cdleme42ke  40468  dia2dimlem13  41059  dvh4dimN  41430  mapdval4N  41615  ccatcan2d  42271  zdivgd  42351  cnreeu  42477  sineq0ALT  44935  cncfiooicc  45850  fourierdlem41  46104  fourierdlem71  46133  bgoldbtbndlem4  47733  bgoldbtbnd  47734  isubgr3stgrlem8  47876