Theorem sylan9req 2664

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602

This theorem is referenced by:  ordintdif  5676  fndmu  5891  fodmrnu  6020  funcoeqres  6064  tz7.44-3  7368  dfac5lem4  8809  zdiv  11281  hashimarni  13040  ccatws1lenrev  13208  fprodss  14465  dvdsmulc  14795  smumullem  15000  cncongrcoprm  15170  mgmidmo  17030  reslmhm2b  18823  fclsfnflim  21588  ustuqtop1  21802  ulm2  23887  sineq0  24021  cxple2a  24189  sqff1o  24652  lgsmodeq  24811  eedimeq  25523  grpoidinvlem4  26538  hlimuni  27272  dmdsl3  28351  atoml2i  28419  disjpreima  28572  sspreima  28620  xrge0npcan  28818  poimirlem3  32365  poimirlem4  32366  poimirlem16  32378  poimirlem17  32379  poimirlem19  32381  poimirlem20  32382  poimirlem23  32385  poimirlem24  32386  poimirlem25  32387  poimirlem29  32391  poimirlem31  32393  eqfnun  32469  ltrncnvnid  34214  cdleme20j  34407  cdleme42ke  34574  dia2dimlem13  35166  dvh4dimN  35537  mapdval4N  35722  sineq0ALT  37978  cncfiooicc  38563  fourierdlem41  38824  fourierdlem71  38853  bgoldbtbndlem4  40008  bgoldbtbnd  40009