Theorem sylan9req 2796

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  ordintdif  6368  fndmu  6599  fodmrnu  6754  funcoeqres  6805  eqfnun  6985  sspreima  7016  tz7.44-3  8344  fsetfocdm  8805  dfac5lem4  10046  dfac5lem4OLD  10048  zdiv  12597  hashimarni  14401  fprodss  15911  dvdsmulc  16250  smumullem  16459  cncongrcoprm  16637  mgmidmo  18626  reslmhm2b  21051  fclsfnflim  24017  ustuqtop1  24231  ulm2  26375  sineq0  26513  cxple2a  26688  sqff1o  27170  lgsmodeq  27330  eedimeq  28992  frrusgrord0  30435  grpoidinvlem4  30603  hlimuni  31334  dmdsl3  32411  atoml2i  32479  disjpreima  32680  xrge0npcan  33106  poimirlem3  37991  poimirlem4  37992  poimirlem16  38004  poimirlem17  38005  poimirlem19  38007  poimirlem20  38008  poimirlem23  38011  poimirlem24  38012  poimirlem25  38013  poimirlem29  38017  poimirlem31  38019  unidmqs  39107  ltrncnvnid  40620  cdleme20j  40811  cdleme42ke  40978  dia2dimlem13  41569  dvh4dimN  41940  mapdval4N  42125  ccatcan2d  42736  zdivgd  42815  cnreeu  42981  sineq0ALT  45381  cncfiooicc  46338  fourierdlem41  46592  fourierdlem71  46621  bgoldbtbndlem4  48300  bgoldbtbnd  48301  isubgr3stgrlem8  48465  prcof1  49879