Theorem sylan9req 2798

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  ordintdif  6434  fndmu  6675  fodmrnu  6828  funcoeqres  6879  eqfnun  7057  sspreima  7088  tz7.44-3  8448  fsetfocdm  8901  dfac5lem4  10166  dfac5lem4OLD  10168  zdiv  12688  hashimarni  14480  fprodss  15984  dvdsmulc  16321  smumullem  16529  cncongrcoprm  16707  mgmidmo  18673  reslmhm2b  21053  fclsfnflim  24035  ustuqtop1  24250  ulm2  26428  sineq0  26566  cxple2a  26741  sqff1o  27225  lgsmodeq  27386  eedimeq  28913  frrusgrord0  30359  grpoidinvlem4  30526  hlimuni  31257  dmdsl3  32334  atoml2i  32402  disjpreima  32597  xrge0npcan  33025  poimirlem3  37630  poimirlem4  37631  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem29  37656  poimirlem31  37658  unidmqs  38655  ltrncnvnid  40129  cdleme20j  40320  cdleme42ke  40487  dia2dimlem13  41078  dvh4dimN  41449  mapdval4N  41634  ccatcan2d  42292  zdivgd  42372  cnreeu  42500  sineq0ALT  44957  cncfiooicc  45909  fourierdlem41  46163  fourierdlem71  46192  bgoldbtbndlem4  47795  bgoldbtbnd  47796  isubgr3stgrlem8  47940