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

Theorem sylan9req 2877
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 2827 . 2 (𝜑𝐴 = 𝐵)
3 sylan9req.2 . 2 (𝜓𝐵 = 𝐶)
42, 3sylan9eq 2876 1 ((𝜑𝜓) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2814
This theorem is referenced by:  ordintdif  6213  fndmu  6431  fodmrnu  6571  funcoeqres  6618  tz7.44-3  8019  dfac5lem4  9529  zdiv  12030  hashimarni  13786  fprodss  15281  dvdsmulc  15616  smumullem  15818  cncongrcoprm  15991  mgmidmo  17849  reslmhm2b  19802  fclsfnflim  22611  ustuqtop1  22826  ulm2  24959  sineq0  25095  cxple2a  25269  sqff1o  25746  lgsmodeq  25905  eedimeq  26671  frrusgrord0  28104  grpoidinvlem4  28269  hlimuni  29000  dmdsl3  30077  atoml2i  30145  disjpreima  30321  sspreima  30379  xrge0npcan  30689  poimirlem3  34942  poimirlem4  34943  poimirlem16  34955  poimirlem17  34956  poimirlem19  34958  poimirlem20  34959  poimirlem23  34962  poimirlem24  34963  poimirlem25  34964  poimirlem29  34968  poimirlem31  34970  eqfnun  35042  unidmqs  35930  ltrncnvnid  37305  cdleme20j  37496  cdleme42ke  37663  dia2dimlem13  38254  dvh4dimN  38625  mapdval4N  38810  ccatcan2d  39253  sineq0ALT  41454  cncfiooicc  42355  fourierdlem41  42609  fourierdlem71  42638  bgoldbtbndlem4  44145  bgoldbtbnd  44146
  Copyright terms: Public domain W3C validator