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

Theorem dedth 4484
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 4491. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4497 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4497. (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 4434 . . . 4 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
32eqcomd 2807 . . 3 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
4 dedth.1 . . 3 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜒))
53, 4syl 17 . 2 (𝜑 → (𝜓𝜒))
61, 5mpbiri 261 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  ifcif 4428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-if 4429
This theorem is referenced by:  dedth2h  4485  dedth3h  4486  orduninsuc  7542  oeoe  8212  limensuc  8682  axcc4dom  9856  inar1  10190  supsr  10527  renegcl  10942  peano5uzti  12064  uzenom  13331  seqfn  13380  seq1  13381  seqp1  13383  hashxp  13795  smadiadetr  21283  imsmet  28477  smcn  28484  nmlno0i  28580  nmblolbi  28586  blocn  28593  dipdir  28628  dipass  28631  siilem2  28638  htth  28704  normlem6  28901  normlem7tALT  28905  normsq  28920  hhssablo  29049  hhssnvt  29051  hhsssh  29055  shintcl  29116  chintcl  29118  pjhth  29179  ococ  29192  chm0  29277  chne0  29280  chocin  29281  chj0  29283  chjo  29301  h1de2ci  29342  spansn  29345  elspansn  29352  pjch1  29456  pjinormi  29473  pjige0  29477  hoaddid1  29577  hodid  29578  nmlnop0  29784  lnopunilem2  29797  elunop2  29799  lnophm  29805  nmbdoplb  29811  nmcopex  29815  nmcoplb  29816  lnopcon  29821  lnfn0  29833  lnfnmul  29834  nmbdfnlb  29836  nmcfnex  29839  nmcfnlb  29840  lnfncon  29842  riesz4  29850  riesz1  29851  cnlnadjeu  29864  pjhmop  29936  hmopidmch  29939  hmopidmpj  29940  pjss2coi  29950  pjssmi  29951  pjssge0i  29952  pjdifnormi  29953  pjidmco  29967  mdslmd1lem3  30113  mdslmd1lem4  30114  csmdsymi  30120  hatomic  30146  atord  30174  atcvat2  30175  chirred  30181  bnj941  32152  bnj944  32318  sqdivzi  33067  onsucconn  33894  onsucsuccmp  33900  limsucncmp  33902  dedths  36251  dedths2  36254  bnd2d  45198
  Copyright terms: Public domain W3C validator