Theorem sylan9req 2801

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  ordintdif  6445  fndmu  6686  fodmrnu  6842  funcoeqres  6893  eqfnun  7070  sspreima  7101  tz7.44-3  8464  fsetfocdm  8919  dfac5lem4  10195  dfac5lem4OLD  10197  zdiv  12713  hashimarni  14490  fprodss  15996  dvdsmulc  16332  smumullem  16538  cncongrcoprm  16717  mgmidmo  18698  reslmhm2b  21076  fclsfnflim  24056  ustuqtop1  24271  ulm2  26446  sineq0  26584  cxple2a  26759  sqff1o  27243  lgsmodeq  27404  eedimeq  28931  frrusgrord0  30372  grpoidinvlem4  30539  hlimuni  31270  dmdsl3  32347  atoml2i  32415  disjpreima  32606  xrge0npcan  33006  poimirlem3  37583  poimirlem4  37584  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem29  37609  poimirlem31  37611  unidmqs  38610  ltrncnvnid  40084  cdleme20j  40275  cdleme42ke  40442  dia2dimlem13  41033  dvh4dimN  41404  mapdval4N  41589  ccatcan2d  42246  zdivgd  42324  cnreeu  42446  sineq0ALT  44908  cncfiooicc  45815  fourierdlem41  46069  fourierdlem71  46098  bgoldbtbndlem4  47682  bgoldbtbnd  47683