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

Theorem sylan9req 2826
 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 2777 . 2 (𝜑𝐴 = 𝐵)
3 sylan9req.2 . 2 (𝜓𝐵 = 𝐶)
42, 3sylan9eq 2825 1 ((𝜑𝜓) → 𝐴 = 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764 This theorem is referenced by:  ordintdif  5916  fndmu  6131  fodmrnu  6265  funcoeqres  6309  tz7.44-3  7661  dfac5lem4  9153  zdiv  11654  hashimarni  13430  ccatws1lenrevOLD  13615  fprodss  14885  dvdsmulc  15218  smumullem  15422  cncongrcoprm  15591  mgmidmo  17467  reslmhm2b  19267  fclsfnflim  22051  ustuqtop1  22265  ulm2  24359  sineq0  24494  cxple2a  24666  sqff1o  25129  lgsmodeq  25288  eedimeq  25999  frrusgrord0  27522  grpoidinvlem4  27701  hlimuni  28435  dmdsl3  29514  atoml2i  29582  disjpreima  29735  sspreima  29787  xrge0npcan  30034  poimirlem3  33745  poimirlem4  33746  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem23  33765  poimirlem24  33766  poimirlem25  33767  poimirlem29  33771  poimirlem31  33773  eqfnun  33848  ltrncnvnid  35936  cdleme20j  36128  cdleme42ke  36295  dia2dimlem13  36886  dvh4dimN  37257  mapdval4N  37442  sineq0ALT  39695  cncfiooicc  40622  fourierdlem41  40879  fourierdlem71  40908  bgoldbtbndlem4  42221  bgoldbtbnd  42222
 Copyright terms: Public domain W3C validator