MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dedth Unicode version

Theorem dedth 3993
Description: Weak deduction theorem that eliminates a hypothesis , making it become an antecedent. We assume that a proof exists for when the class variable is replaced with a specific class . The hypothesis should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 4000. If the inference has other hypotheses with class variable , these can be kept by assigning keephyp 4006 to them. For more information, see the Deduction Theorem http://us.metamath.org/mpeuni/mmdeduction.html. (Contributed by NM, 15-May-1999.)
Hypotheses
Ref Expression
dedth.1
dedth.2
Assertion
Ref Expression
dedth

Proof of Theorem dedth
StepHypRef Expression
1 dedth.2 . 2
2 iftrue 3947 . . . 4
32eqcomd 2465 . . 3
4 dedth.1 . . 3
53, 4syl 16 . 2
61, 5mpbiri 233 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  ifcif 3941
This theorem is referenced by:  dedth2h  3994  dedth3h  3995  orduninsuc  6678  oeoe  7267  limensuc  7714  axcc4dom  8842  inar1  9174  supsr  9510  renegcl  9905  peano5uzti  10977  uzenom  12075  seqfn  12119  seq1  12120  seqp1  12122  hashxp  12492  smadiadetr  19177  imsmet  25597  smcn  25608  nmlno0i  25709  nmblolbi  25715  blocn  25722  dipdir  25757  dipass  25760  siilem2  25767  htth  25835  normlem6  26032  normlem7tALT  26036  normsq  26051  hhssablo  26179  hhssnvt  26181  hhsssh  26185  shintcl  26248  chintcl  26250  pjhth  26311  ococ  26324  chm0  26409  chne0  26412  chocin  26413  chj0  26415  chjo  26433  h1de2ci  26474  spansn  26477  elspansn  26484  pjch1  26588  pjinormi  26605  pjige0  26609  hoaddid1  26710  hodid  26711  nmlnop0  26917  lnopunilem2  26930  elunop2  26932  lnophm  26938  nmbdoplb  26944  nmcopex  26948  nmcoplb  26949  lnopcon  26954  lnfn0  26966  lnfnmul  26967  nmbdfnlb  26969  nmcfnex  26972  nmcfnlb  26973  lnfncon  26975  riesz4  26983  riesz1  26984  cnlnadjeu  26997  pjhmop  27069  hmopidmch  27072  hmopidmpj  27073  pjss2coi  27083  pjssmi  27084  pjssge0i  27085  pjdifnormi  27086  pjidmco  27100  mdslmd1lem3  27246  mdslmd1lem4  27247  csmdsymi  27253  hatomic  27279  atord  27307  atcvat2  27308  chirred  27314  sqdivzi  29104  onsuccon  29903  onsucsuccmp  29909  limsucncmp  29911  bnj941  33831  bnj944  33996  dedths  34693  dedths2  34696
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942
  Copyright terms: Public domain W3C validator