Theorem sylan9req 2819

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  ordintdif  6432  fndmu  6668  fodmrnu  6826  funcoeqres  6879  eqfnun  7059  sspreima  7091  tz7.44-3  8444  fsetfocdm  8911  dfac5lem4  10232  zdiv  12796  hashimarni  14613  fprodss  16144  dvdsmulc  16482  smumullem  16691  cncongrcoprm  16874  mgmidmo  18867  reslmhm2b  21359  fclsfnflim  24376  ustuqtop1  24590  ulm2  26742  sineq0  26882  cxple2a  27057  sqff1o  27539  lgsmodeq  27699  eedimeq  29506  frrusgrord0  30971  grpoidinvlem4  31139  hlimuni  31870  dmdsl3  32947  atoml2i  33015  disjpreima  33250  xrge0npcan  33651  poimirlem3  38733  poimirlem4  38734  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  poimirlem23  38753  poimirlem24  38754  poimirlem25  38755  poimirlem29  38759  poimirlem31  38761  unidmqs  39863  ltrncnvnid  41376  cdleme20j  41567  cdleme42ke  41734  dia2dimlem13  42325  dvh4dimN  42696  mapdval4N  42881  ccatcan2d  43495  zdivgd  43581  cnreeu  43747  sineq0ALT  46110  cncfiooicc  47109  fourierdlem41  47363  fourierdlem71  47392  bgoldbtbndlem4  49111  bgoldbtbnd  49112  isubgr3stgrlem8  49276  prcof1  50728