Theorem sylan9req 2791

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 2790	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  ordintdif  6403  fndmu  6645  fodmrnu  6798  funcoeqres  6849  eqfnun  7027  sspreima  7058  tz7.44-3  8422  fsetfocdm  8875  dfac5lem4  10140  dfac5lem4OLD  10142  zdiv  12663  hashimarni  14459  fprodss  15964  dvdsmulc  16303  smumullem  16511  cncongrcoprm  16689  mgmidmo  18638  reslmhm2b  21012  fclsfnflim  23965  ustuqtop1  24180  ulm2  26346  sineq0  26485  cxple2a  26660  sqff1o  27144  lgsmodeq  27305  eedimeq  28877  frrusgrord0  30321  grpoidinvlem4  30488  hlimuni  31219  dmdsl3  32296  atoml2i  32364  disjpreima  32565  xrge0npcan  33015  poimirlem3  37647  poimirlem4  37648  poimirlem16  37660  poimirlem17  37661  poimirlem19  37663  poimirlem20  37664  poimirlem23  37667  poimirlem24  37668  poimirlem25  37669  poimirlem29  37673  poimirlem31  37675  unidmqs  38672  ltrncnvnid  40146  cdleme20j  40337  cdleme42ke  40504  dia2dimlem13  41095  dvh4dimN  41466  mapdval4N  41651  ccatcan2d  42302  zdivgd  42386  cnreeu  42513  sineq0ALT  44961  cncfiooicc  45923  fourierdlem41  46177  fourierdlem71  46206  bgoldbtbndlem4  47822  bgoldbtbnd  47823  isubgr3stgrlem8  47985  prcof1  49298