Theorem sylan9req 2793

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  ordintdif  6366  fndmu  6597  fodmrnu  6752  funcoeqres  6803  eqfnun  6981  sspreima  7012  tz7.44-3  8338  fsetfocdm  8799  dfac5lem4  10037  dfac5lem4OLD  10039  zdiv  12588  hashimarni  14392  fprodss  15902  dvdsmulc  16241  smumullem  16450  cncongrcoprm  16628  mgmidmo  18617  reslmhm2b  21039  fclsfnflim  24001  ustuqtop1  24215  ulm2  26365  sineq0  26504  cxple2a  26679  sqff1o  27163  lgsmodeq  27324  eedimeq  28986  frrusgrord0  30430  grpoidinvlem4  30598  hlimuni  31329  dmdsl3  32406  atoml2i  32474  disjpreima  32674  xrge0npcan  33100  poimirlem3  37955  poimirlem4  37956  poimirlem16  37968  poimirlem17  37969  poimirlem19  37971  poimirlem20  37972  poimirlem23  37975  poimirlem24  37976  poimirlem25  37977  poimirlem29  37981  poimirlem31  37983  unidmqs  39071  ltrncnvnid  40584  cdleme20j  40775  cdleme42ke  40942  dia2dimlem13  41533  dvh4dimN  41904  mapdval4N  42089  ccatcan2d  42701  zdivgd  42780  cnreeu  42946  sineq0ALT  45378  cncfiooicc  46337  fourierdlem41  46591  fourierdlem71  46620  bgoldbtbndlem4  48281  bgoldbtbnd  48282  isubgr3stgrlem8  48446  prcof1  49860