Theorem sylan9req 2794

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  ordintdif  6415  fndmu  6657  fodmrnu  6814  funcoeqres  6865  eqfnun  7039  sspreima  7070  tz7.44-3  8408  dfac5lem4  10121  zdiv  12632  hashimarni  14401  fprodss  15892  dvdsmulc  16227  smumullem  16433  cncongrcoprm  16607  mgmidmo  18579  reslmhm2b  20665  fclsfnflim  23531  ustuqtop1  23746  ulm2  25897  sineq0  26033  cxple2a  26207  sqff1o  26686  lgsmodeq  26845  eedimeq  28156  frrusgrord0  29593  grpoidinvlem4  29760  hlimuni  30491  dmdsl3  31568  atoml2i  31636  disjpreima  31815  xrge0npcan  32195  poimirlem3  36491  poimirlem4  36492  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem29  36517  poimirlem31  36519  unidmqs  37524  ltrncnvnid  38998  cdleme20j  39189  cdleme42ke  39356  dia2dimlem13  39947  dvh4dimN  40318  mapdval4N  40503  ccatcan2d  41069  cnreeu  41341  sineq0ALT  43698  cncfiooicc  44610  fourierdlem41  44864  fourierdlem71  44893  bgoldbtbndlem4  46476  bgoldbtbnd  46477