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  6375  fndmu  6606  fodmrnu  6761  funcoeqres  6812  eqfnun  6990  sspreima  7021  tz7.44-3  8347  fsetfocdm  8808  dfac5lem4  10048  dfac5lem4OLD  10050  zdiv  12599  hashimarni  14403  fprodss  15913  dvdsmulc  16252  smumullem  16461  cncongrcoprm  16639  mgmidmo  18628  reslmhm2b  21049  fclsfnflim  23992  ustuqtop1  24206  ulm2  26350  sineq0  26488  cxple2a  26663  sqff1o  27145  lgsmodeq  27305  eedimeq  28967  frrusgrord0  30410  grpoidinvlem4  30578  hlimuni  31309  dmdsl3  32386  atoml2i  32454  disjpreima  32654  xrge0npcan  33080  poimirlem3  37944  poimirlem4  37945  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem29  37970  poimirlem31  37972  unidmqs  39060  ltrncnvnid  40573  cdleme20j  40764  cdleme42ke  40931  dia2dimlem13  41522  dvh4dimN  41893  mapdval4N  42078  ccatcan2d  42690  zdivgd  42769  cnreeu  42935  sineq0ALT  45363  cncfiooicc  46322  fourierdlem41  46576  fourierdlem71  46605  bgoldbtbndlem4  48278  bgoldbtbnd  48279  isubgr3stgrlem8  48443  prcof1  49857