Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9req Structured version   Visualization version   GIF version

Theorem sylan9req 2665
 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
StepHypRef Expression
1 sylan9req.1 . . 3 (𝜑𝐵 = 𝐴)
21eqcomd 2616 . 2 (𝜑𝐴 = 𝐵)
3 sylan9req.2 . 2 (𝜓𝐵 = 𝐶)
42, 3sylan9eq 2664 1 ((𝜑𝜓) → 𝐴 = 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603 This theorem is referenced by:  ordintdif  5691  fndmu  5906  fodmrnu  6036  funcoeqres  6080  tz7.44-3  7391  dfac5lem4  8832  zdiv  11323  hashimarni  13086  ccatws1lenrev  13260  fprodss  14517  dvdsmulc  14847  smumullem  15052  cncongrcoprm  15222  mgmidmo  17082  reslmhm2b  18875  fclsfnflim  21641  ustuqtop1  21855  ulm2  23943  sineq0  24077  cxple2a  24245  sqff1o  24708  lgsmodeq  24867  eedimeq  25578  grpoidinvlem4  26745  hlimuni  27479  dmdsl3  28558  atoml2i  28626  disjpreima  28779  sspreima  28827  xrge0npcan  29025  poimirlem3  32582  poimirlem4  32583  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem29  32608  poimirlem31  32610  eqfnun  32686  ltrncnvnid  34431  cdleme20j  34624  cdleme42ke  34791  dia2dimlem13  35383  dvh4dimN  35754  mapdval4N  35939  sineq0ALT  38195  cncfiooicc  38780  fourierdlem41  39041  fourierdlem71  39070  bgoldbtbndlem4  40224  bgoldbtbnd  40225
 Copyright terms: Public domain W3C validator