Theorem sylan9req 2816

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 2815	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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  ordintdif  6403  fndmu  6634  fodmrnu  6792  funcoeqres  6844  eqfnun  7024  sspreima  7055  tz7.44-3  8394  fsetfocdm  8861  dfac5lem4  10177  zdiv  12739  hashimarni  14554  fprodss  16083  dvdsmulc  16421  smumullem  16630  cncongrcoprm  16808  mgmidmo  18800  reslmhm2b  21291  fclsfnflim  24308  ustuqtop1  24522  ulm2  26676  sineq0  26816  cxple2a  26991  sqff1o  27473  lgsmodeq  27633  eedimeq  29410  frrusgrord0  30875  grpoidinvlem4  31043  hlimuni  31774  dmdsl3  32851  atoml2i  32919  disjpreima  33112  xrge0npcan  33515  poimirlem3  38461  poimirlem4  38462  poimirlem16  38474  poimirlem17  38475  poimirlem19  38477  poimirlem20  38478  poimirlem23  38481  poimirlem24  38482  poimirlem25  38483  poimirlem29  38487  poimirlem31  38489  unidmqs  39591  ltrncnvnid  41104  cdleme20j  41295  cdleme42ke  41462  dia2dimlem13  42053  dvh4dimN  42424  mapdval4N  42609  ccatcan2d  43222  zdivgd  43316  cnreeu  43482  sineq0ALT  45863  cncfiooicc  46826  fourierdlem41  47080  fourierdlem71  47109  bgoldbtbndlem4  48828  bgoldbtbnd  48829  isubgr3stgrlem8  48993  prcof1  50418