Theorem sylan9req 2821

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757

This theorem is referenced by:  ordintdif  6401  fndmu  6632  fodmrnu  6790  funcoeqres  6842  eqfnun  7022  sspreima  7053  tz7.44-3  8383  fsetfocdm  8846  dfac5lem4  10098  zdiv  12657  hashimarni  14468  fprodss  15992  dvdsmulc  16331  smumullem  16540  cncongrcoprm  16718  mgmidmo  18708  reslmhm2b  21144  fclsfnflim  24145  ustuqtop1  24359  ulm2  26506  sineq0  26647  cxple2a  26822  sqff1o  27304  lgsmodeq  27464  eedimeq  29157  frrusgrord0  30600  grpoidinvlem4  30768  hlimuni  31499  dmdsl3  32576  atoml2i  32644  disjpreima  32839  xrge0npcan  33253  poimirlem3  38134  poimirlem4  38135  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem23  38154  poimirlem24  38155  poimirlem25  38156  poimirlem29  38160  poimirlem31  38162  unidmqs  39250  ltrncnvnid  40763  cdleme20j  40954  cdleme42ke  41121  dia2dimlem13  41712  dvh4dimN  42083  mapdval4N  42268  ccatcan2d  42879  zdivgd  42958  cnreeu  43124  sineq0ALT  45510  cncfiooicc  46466  fourierdlem41  46720  fourierdlem71  46749  bgoldbtbndlem4  48428  bgoldbtbnd  48429  isubgr3stgrlem8  48593  prcof1  50017