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 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.) |
Ref | Expression |
---|---|
dedth.1 | ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒)) |
dedth.2 | ⊢ 𝜒 |
Ref | Expression |
---|---|
dedth | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dedth.2 | . 2 ⊢ 𝜒 | |
2 | iftrue 4469 | . . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2824 | . . 3 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | dedth.1 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒)) | |
5 | 3, 4 | syl 17 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
6 | 1, 5 | mpbiri 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 |