![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dedth | Structured version Visualization version GIF version |
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's hypothesis eliminated with elimhyp 4179. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4185 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html. (Contributed by NM, 15-May-1999.) |
Ref | Expression |
---|---|
dedth.1 | ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒)) |
dedth.2 | ⊢ 𝜒 |
Ref | Expression |
---|---|
dedth | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dedth.2 | . 2 ⊢ 𝜒 | |
2 | iftrue 4125 | . . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2657 | . . 3 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | dedth.1 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒)) | |
5 | 3, 4 | syl 17 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
6 | 1, 5 | mpbiri 248 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1523 ifcif 4119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-if 4120 |
This theorem is referenced by: dedth2h 4173 dedth3h 4174 orduninsuc 7085 oeoe 7724 limensuc 8178 axcc4dom 9301 inar1 9635 supsr 9971 renegcl 10382 peano5uzti 11505 uzenom 12803 seqfn 12853 seq1 12854 seqp1 12856 hashxp 13259 smadiadetr 20529 imsmet 27674 smcn 27681 nmlno0i 27777 nmblolbi 27783 blocn 27790 dipdir 27825 dipass 27828 siilem2 27835 htth 27903 normlem6 28100 normlem7tALT 28104 normsq 28119 hhssablo 28248 hhssnvt 28250 hhsssh 28254 shintcl 28317 chintcl 28319 pjhth 28380 ococ 28393 chm0 28478 chne0 28481 chocin 28482 chj0 28484 chjo 28502 h1de2ci 28543 spansn 28546 elspansn 28553 pjch1 28657 pjinormi 28674 pjige0 28678 hoaddid1 28778 hodid 28779 nmlnop0 28985 lnopunilem2 28998 elunop2 29000 lnophm 29006 nmbdoplb 29012 nmcopex 29016 nmcoplb 29017 lnopcon 29022 lnfn0 29034 lnfnmul 29035 nmbdfnlb 29037 nmcfnex 29040 nmcfnlb 29041 lnfncon 29043 riesz4 29051 riesz1 29052 cnlnadjeu 29065 pjhmop 29137 hmopidmch 29140 hmopidmpj 29141 pjss2coi 29151 pjssmi 29152 pjssge0i 29153 pjdifnormi 29154 pjidmco 29168 mdslmd1lem3 29314 mdslmd1lem4 29315 csmdsymi 29321 hatomic 29347 atord 29375 atcvat2 29376 chirred 29382 bnj941 30969 bnj944 31134 sqdivzi 31736 onsucconn 32562 onsucsuccmp 32568 limsucncmp 32570 dedths 34566 dedths2 34569 bnd2d 42753 |
Copyright terms: Public domain | W3C validator |