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

Theorem sylan9req 2794
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 2739 . 2 (𝜑𝐴 = 𝐵)
3 sylan9req.2 . 2 (𝜓𝐵 = 𝐶)
42, 3sylan9eq 2793 1 ((𝜑𝜓) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725
This theorem is referenced by:  ordintdif  6371  fndmu  6613  fodmrnu  6768  funcoeqres  6819  sspreima  7022  tz7.44-3  8358  dfac5lem4  10070  zdiv  12581  hashimarni  14350  fprodss  15839  dvdsmulc  16174  smumullem  16380  cncongrcoprm  16554  mgmidmo  18523  reslmhm2b  20559  fclsfnflim  23401  ustuqtop1  23616  ulm2  25767  sineq0  25903  cxple2a  26077  sqff1o  26554  lgsmodeq  26713  eedimeq  27896  frrusgrord0  29333  grpoidinvlem4  29498  hlimuni  30229  dmdsl3  31306  atoml2i  31374  disjpreima  31555  xrge0npcan  31941  poimirlem3  36131  poimirlem4  36132  poimirlem16  36144  poimirlem17  36145  poimirlem19  36147  poimirlem20  36148  poimirlem23  36151  poimirlem24  36152  poimirlem25  36153  poimirlem29  36157  poimirlem31  36159  eqfnun  36231  unidmqs  37166  ltrncnvnid  38640  cdleme20j  38831  cdleme42ke  38998  dia2dimlem13  39589  dvh4dimN  39960  mapdval4N  40145  ccatcan2d  40717  cnreeu  40984  sineq0ALT  43311  cncfiooicc  44225  fourierdlem41  44479  fourierdlem71  44508  bgoldbtbndlem4  46090  bgoldbtbnd  46091
  Copyright terms: Public domain W3C validator