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  6376  fndmu  6607  fodmrnu  6762  funcoeqres  6813  eqfnun  6991  sspreima  7022  tz7.44-3  8349  fsetfocdm  8810  dfac5lem4  10048  dfac5lem4OLD  10050  zdiv  12574  hashimarni  14376  fprodss  15883  dvdsmulc  16222  smumullem  16431  cncongrcoprm  16609  mgmidmo  18597  reslmhm2b  21018  fclsfnflim  23983  ustuqtop1  24197  ulm2  26362  sineq0  26501  cxple2a  26676  sqff1o  27160  lgsmodeq  27321  eedimeq  28983  frrusgrord0  30427  grpoidinvlem4  30594  hlimuni  31325  dmdsl3  32402  atoml2i  32470  disjpreima  32670  xrge0npcan  33112  poimirlem3  37863  poimirlem4  37864  poimirlem16  37876  poimirlem17  37877  poimirlem19  37879  poimirlem20  37880  poimirlem23  37883  poimirlem24  37884  poimirlem25  37885  poimirlem29  37889  poimirlem31  37891  unidmqs  38979  ltrncnvnid  40492  cdleme20j  40683  cdleme42ke  40850  dia2dimlem13  41441  dvh4dimN  41812  mapdval4N  41997  ccatcan2d  42610  zdivgd  42696  cnreeu  42849  sineq0ALT  45281  cncfiooicc  46241  fourierdlem41  46495  fourierdlem71  46524  bgoldbtbndlem4  48157  bgoldbtbnd  48158  isubgr3stgrlem8  48322  prcof1  49736