Theorem sylan9req 2854

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  ordintdif  6208  fndmu  6429  fodmrnu  6573  funcoeqres  6620  tz7.44-3  8027  dfac5lem4  9537  zdiv  12040  hashimarni  13798  fprodss  15294  dvdsmulc  15629  smumullem  15831  cncongrcoprm  16004  mgmidmo  17862  reslmhm2b  19819  fclsfnflim  22632  ustuqtop1  22847  ulm2  24980  sineq0  25116  cxple2a  25290  sqff1o  25767  lgsmodeq  25926  eedimeq  26692  frrusgrord0  28125  grpoidinvlem4  28290  hlimuni  29021  dmdsl3  30098  atoml2i  30166  disjpreima  30347  sspreima  30406  xrge0npcan  30728  poimirlem3  35060  poimirlem4  35061  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem29  35086  poimirlem31  35088  eqfnun  35160  unidmqs  36048  ltrncnvnid  37423  cdleme20j  37614  cdleme42ke  37781  dia2dimlem13  38372  dvh4dimN  38743  mapdval4N  38928  ccatcan2d  39422  cnreeu  39593  sineq0ALT  41643  cncfiooicc  42536  fourierdlem41  42790  fourierdlem71  42819  bgoldbtbndlem4  44326  bgoldbtbnd  44327