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

Theorem dedth 4519
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 hypothesis eliminated with elimhyp 4526. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4532 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4532. (Contributed by NM, 15-May-1999.)
Hypotheses
Ref Expression
dedth.1 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜒))
dedth.2 𝜒
Assertion
Ref Expression
dedth (𝜑𝜓)

Proof of Theorem dedth
StepHypRef Expression
1 dedth.2 . 2 𝜒
2 iftrue 4469 . . . 4 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
32eqcomd 2824 . . 3 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
4 dedth.1 . . 3 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜒))
53, 4syl 17 . 2 (𝜑 → (𝜓𝜒))
61, 5mpbiri 259 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  ifcif 4463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-if 4464
This theorem is referenced by:  dedth2h  4520  dedth3h  4521  orduninsuc  7547  oeoe  8214  limensuc  8682  axcc4dom  9851  inar1  10185  supsr  10522  renegcl  10937  peano5uzti  12060  uzenom  13320  seqfn  13369  seq1  13370  seqp1  13372  hashxp  13783  smadiadetr  21212  imsmet  28395  smcn  28402  nmlno0i  28498  nmblolbi  28504  blocn  28511  dipdir  28546  dipass  28549  siilem2  28556  htth  28622  normlem6  28819  normlem7tALT  28823  normsq  28838  hhssablo  28967  hhssnvt  28969  hhsssh  28973  shintcl  29034  chintcl  29036  pjhth  29097  ococ  29110  chm0  29195  chne0  29198  chocin  29199  chj0  29201  chjo  29219  h1de2ci  29260  spansn  29263  elspansn  29270  pjch1  29374  pjinormi  29391  pjige0  29395  hoaddid1  29495  hodid  29496  nmlnop0  29702  lnopunilem2  29715  elunop2  29717  lnophm  29723  nmbdoplb  29729  nmcopex  29733  nmcoplb  29734  lnopcon  29739  lnfn0  29751  lnfnmul  29752  nmbdfnlb  29754  nmcfnex  29757  nmcfnlb  29758  lnfncon  29760  riesz4  29768  riesz1  29769  cnlnadjeu  29782  pjhmop  29854  hmopidmch  29857  hmopidmpj  29858  pjss2coi  29868  pjssmi  29869  pjssge0i  29870  pjdifnormi  29871  pjidmco  29885  mdslmd1lem3  30031  mdslmd1lem4  30032  csmdsymi  30038  hatomic  30064  atord  30092  atcvat2  30093  chirred  30099  bnj941  31943  bnj944  32109  sqdivzi  32856  onsucconn  33683  onsucsuccmp  33689  limsucncmp  33691  dedths  35978  dedths2  35981  bnd2d  44712
  Copyright terms: Public domain W3C validator