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

Theorem dedth 3952
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 3959. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 3965 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 3908 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2462 . . 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 233 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1370   ifcif 3902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3903
This theorem is referenced by:  dedth2h  3953  dedth3h  3954  orduninsuc  6567  oeoe  7151  limensuc  7601  axcc4dom  8724  inar1  9056  supsr  9393  renegcl  9786  peano5uzti  10845  uzenom  11907  seqfn  11938  seq1  11939  seqp1  11941  hashxp  12317  smadiadetr  18616  imsmet  24254  smcn  24265  nmlno0i  24366  nmblolbi  24372  blocn  24379  dipdir  24414  dipass  24417  siilem2  24424  htth  24492  normlem6  24689  normlem7tALT  24693  normsq  24708  hhssablo  24836  hhssnvt  24838  hhsssh  24842  shintcl  24905  chintcl  24907  pjhth  24968  ococ  24981  chm0  25066  chne0  25069  chocin  25070  chj0  25072  chjo  25090  h1de2ci  25131  spansn  25134  elspansn  25141  pjch1  25245  pjinormi  25262  pjige0  25266  hoaddid1  25367  hodid  25368  nmlnop0  25574  lnopunilem2  25587  elunop2  25589  lnophm  25595  nmbdoplb  25601  nmcopex  25605  nmcoplb  25606  lnopcon  25611  lnfn0  25623  lnfnmul  25624  nmbdfnlb  25626  nmcfnex  25629  nmcfnlb  25630  lnfncon  25632  riesz4  25640  riesz1  25641  cnlnadjeu  25654  pjhmop  25726  hmopidmch  25729  hmopidmpj  25730  pjss2coi  25740  pjssmi  25741  pjssge0i  25742  pjdifnormi  25743  pjidmco  25757  mdslmd1lem3  25903  mdslmd1lem4  25904  csmdsymi  25910  hatomic  25936  atord  25964  atcvat2  25965  chirred  25971  sqdivzi  27547  onsuccon  28448  onsucsuccmp  28454  limsucncmp  28456  bnj941  32118  bnj944  32283  dedths  32971  dedths2  32974
  Copyright terms: Public domain W3C validator