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

Theorem dedth 3809
Description: Weak deduction theorem that eliminates a hypothesis 
ph, making it become an antecedent. We assume that a proof exists for  ph when the class variable  A is replaced with a specific class 
B. The hypothesis  ch should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 3816. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 3822 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  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  ch )
)
dedth.2  |-  ch
Assertion
Ref Expression
dedth  |-  ( ph  ->  ps )

Proof of Theorem dedth
StepHypRef Expression
1 dedth.2 . 2  |-  ch
2 iftrue 3773 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2448 . . 3  |-  ( ph  ->  A  =  if (
ph ,  A ,  B ) )
4 dedth.1 . . 3  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  ch )
)
53, 4syl 16 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
61, 5mpbiri 226 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1654   ifcif 3767
This theorem is referenced by:  dedth2h  3810  dedth3h  3811  orduninsuc  4858  oeoe  6878  limensuc  7320  axcc4dom  8359  inar1  8688  supsr  9025  renegcl  9402  peano5uzti  10397  uzenom  11342  seqfn  11373  seq1  11374  seqp1  11376  hashxp  11735  imsmet  22221  smcn  22232  nmlno0i  22333  nmblolbi  22339  blocn  22346  dipdir  22381  dipass  22384  siilem2  22391  htth  22459  normlem6  22655  normlem7tALT  22659  normsq  22674  hhssablo  22801  hhssnvt  22803  hhsssh  22807  shintcl  22870  chintcl  22872  pjhth  22933  ococ  22946  chm0  23031  chne0  23034  chocin  23035  chj0  23037  chjo  23055  h1de2ci  23096  spansn  23099  elspansn  23106  pjch1  23210  pjinormi  23227  pjige0  23231  hoaddid1  23332  hodid  23333  nmlnop0  23539  lnopunilem2  23552  elunop2  23554  lnophm  23560  nmbdoplb  23566  nmcopex  23570  nmcoplb  23571  lnopcon  23576  lnfn0  23588  lnfnmul  23589  nmbdfnlb  23591  nmcfnex  23594  nmcfnlb  23595  lnfncon  23597  riesz4  23605  riesz1  23606  cnlnadjeu  23619  pjhmop  23691  hmopidmch  23694  hmopidmpj  23695  pjss2coi  23705  pjssmi  23706  pjssge0i  23707  pjdifnormi  23708  pjidmco  23722  mdslmd1lem3  23868  mdslmd1lem4  23869  csmdsymi  23875  hatomic  23901  atord  23929  atcvat2  23930  chirred  23936  sqdivzi  25219  onsuccon  26223  onsucsuccmp  26229  limsucncmp  26231  bnj941  29317  bnj944  29483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-if 3768
  Copyright terms: Public domain W3C validator