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

Theorem dedth 3740
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 3747. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 3753 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 3705 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2409 . . 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 225 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   ifcif 3699
This theorem is referenced by:  dedth2h  3741  dedth3h  3742  orduninsuc  4782  oeoe  6801  limensuc  7243  axcc4dom  8277  inar1  8606  supsr  8943  renegcl  9320  peano5uzti  10315  uzenom  11259  seqfn  11290  seq1  11291  seqp1  11293  hashxp  11652  imsmet  22136  smcn  22147  nmlno0i  22248  nmblolbi  22254  blocn  22261  dipdir  22296  dipass  22299  siilem2  22306  htth  22374  normlem6  22570  normlem7tALT  22574  normsq  22589  hhssablo  22716  hhssnvt  22718  hhsssh  22722  shintcl  22785  chintcl  22787  pjhth  22848  ococ  22861  chm0  22946  chne0  22949  chocin  22950  chj0  22952  chjo  22970  h1de2ci  23011  spansn  23014  elspansn  23021  pjch1  23125  pjinormi  23142  pjige0  23146  hoaddid1  23247  hodid  23248  nmlnop0  23454  lnopunilem2  23467  elunop2  23469  lnophm  23475  nmbdoplb  23481  nmcopex  23485  nmcoplb  23486  lnopcon  23491  lnfn0  23503  lnfnmul  23504  nmbdfnlb  23506  nmcfnex  23509  nmcfnlb  23510  lnfncon  23512  riesz4  23520  riesz1  23521  cnlnadjeu  23534  pjhmop  23606  hmopidmch  23609  hmopidmpj  23610  pjss2coi  23620  pjssmi  23621  pjssge0i  23622  pjdifnormi  23623  pjidmco  23637  mdslmd1lem3  23783  mdslmd1lem4  23784  csmdsymi  23790  hatomic  23816  atord  23844  atcvat2  23845  chirred  23851  sqdivzi  25137  onsuccon  26092  onsucsuccmp  26098  limsucncmp  26100  bnj941  28849  bnj944  29015
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-if 3700
  Copyright terms: Public domain W3C validator