Theorem sylan9req 2815

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753

This theorem is referenced by:  ordintdif  5935  fndmu  6153  fodmrnu  6284  funcoeqres  6328  tz7.44-3  7673  dfac5lem4  9139  zdiv  11639  hashimarni  13420  ccatws1lenrevOLD  13606  fprodss  14877  dvdsmulc  15211  smumullem  15416  cncongrcoprm  15586  mgmidmo  17460  reslmhm2b  19256  fclsfnflim  22032  ustuqtop1  22246  ulm2  24338  sineq0  24472  cxple2a  24644  sqff1o  25107  lgsmodeq  25266  eedimeq  25977  frrusgrord0  27494  grpoidinvlem4  27670  hlimuni  28404  dmdsl3  29483  atoml2i  29551  disjpreima  29704  sspreima  29756  xrge0npcan  30003  poimirlem3  33725  poimirlem4  33726  poimirlem16  33738  poimirlem17  33739  poimirlem19  33741  poimirlem20  33742  poimirlem23  33745  poimirlem24  33746  poimirlem25  33747  poimirlem29  33751  poimirlem31  33753  eqfnun  33829  ltrncnvnid  35916  cdleme20j  36108  cdleme42ke  36275  dia2dimlem13  36867  dvh4dimN  37238  mapdval4N  37423  sineq0ALT  39672  cncfiooicc  40610  fourierdlem41  40868  fourierdlem71  40897  bgoldbtbndlem4  42206  bgoldbtbnd  42207