Theorem sylan9req 2800

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  ordintdif  6319  fndmu  6549  fodmrnu  6705  funcoeqres  6756  sspreima  6954  tz7.44-3  8248  dfac5lem4  9891  zdiv  12399  hashimarni  14165  fprodss  15667  dvdsmulc  16002  smumullem  16208  cncongrcoprm  16384  mgmidmo  18353  reslmhm2b  20325  fclsfnflim  23187  ustuqtop1  23402  ulm2  25553  sineq0  25689  cxple2a  25863  sqff1o  26340  lgsmodeq  26499  eedimeq  27275  frrusgrord0  28713  grpoidinvlem4  28878  hlimuni  29609  dmdsl3  30686  atoml2i  30754  disjpreima  30932  xrge0npcan  31312  poimirlem3  35789  poimirlem4  35790  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem29  35815  poimirlem31  35817  eqfnun  35889  unidmqs  36773  ltrncnvnid  38148  cdleme20j  38339  cdleme42ke  38506  dia2dimlem13  39097  dvh4dimN  39468  mapdval4N  39653  ccatcan2d  40226  cnreeu  40445  sineq0ALT  42564  cncfiooicc  43442  fourierdlem41  43696  fourierdlem71  43725  bgoldbtbndlem4  45271  bgoldbtbnd  45272