Theorem sylan9req 2818

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754

This theorem is used by:  ordintdif  6412  fndmu  6642  fodmrnu  6800  funcoeqres  6852  eqfnun  7032  sspreima  7063  tz7.44-3  8393  fsetfocdm  8856  dfac5lem4  10117  zdiv  12672  hashimarni  14485  fprodss  16009  dvdsmulc  16347  smumullem  16556  cncongrcoprm  16734  mgmidmo  18724  reslmhm2b  21186  fclsfnflim  24195  ustuqtop1  24409  ulm2  26559  sineq0  26700  cxple2a  26875  sqff1o  27357  lgsmodeq  27517  eedimeq  29259  frrusgrord0  30702  grpoidinvlem4  30870  hlimuni  31601  dmdsl3  32678  atoml2i  32746  disjpreima  32940  xrge0npcan  33349  poimirlem3  38302  poimirlem4  38303  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem23  38322  poimirlem24  38323  poimirlem25  38324  poimirlem29  38328  poimirlem31  38330  unidmqs  39416  ltrncnvnid  40929  cdleme20j  41120  cdleme42ke  41287  dia2dimlem13  41878  dvh4dimN  42249  mapdval4N  42434  ccatcan2d  43047  zdivgd  43126  cnreeu  43292  sineq0ALT  45673  cncfiooicc  46636  fourierdlem41  46890  fourierdlem71  46919  bgoldbtbndlem4  48601  bgoldbtbnd  48602  isubgr3stgrlem8  48766  prcof1  50194