![]() |
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 4595. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4601 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4601. (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 4536 | . . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2731 | . . 3 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | dedth.1 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒)) | |
5 | 3, 4 | syl 17 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
6 | 1, 5 | mpbiri 257 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ifcif 4530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-if 4531 |
This theorem is referenced by: dedth2h 4589 dedth3h 4590 orduninsuc 7848 oeoe 8620 limensuc 9179 axcc4dom 10466 inar1 10800 supsr 11137 renegcl 11555 peano5uzti 12685 uzenom 13965 seqfn 14014 seq1 14015 seqp1 14017 hashxp 14429 smadiadetr 22621 imsmet 30573 smcn 30580 nmlno0i 30676 nmblolbi 30682 blocn 30689 dipdir 30724 dipass 30727 siilem2 30734 htth 30800 normlem6 30997 normlem7tALT 31001 normsq 31016 hhssablo 31145 hhssnvt 31147 hhsssh 31151 shintcl 31212 chintcl 31214 pjhth 31275 ococ 31288 chm0 31373 chne0 31376 chocin 31377 chj0 31379 chjo 31397 h1de2ci 31438 spansn 31441 elspansn 31448 pjch1 31552 pjinormi 31569 pjige0 31573 hoaddrid 31673 hodid 31674 nmlnop0 31880 lnopunilem2 31893 elunop2 31895 lnophm 31901 nmbdoplb 31907 nmcopex 31911 nmcoplb 31912 lnopcon 31917 lnfn0 31929 lnfnmul 31930 nmbdfnlb 31932 nmcfnex 31935 nmcfnlb 31936 lnfncon 31938 riesz4 31946 riesz1 31947 cnlnadjeu 31960 pjhmop 32032 hmopidmch 32035 hmopidmpj 32036 pjss2coi 32046 pjssmi 32047 pjssge0i 32048 pjdifnormi 32049 pjidmco 32063 mdslmd1lem3 32209 mdslmd1lem4 32210 csmdsymi 32216 hatomic 32242 atord 32270 atcvat2 32271 chirred 32277 bnj941 34534 bnj944 34700 sqdivzi 35453 onsucconn 36053 onsucsuccmp 36059 limsucncmp 36061 dedths 38564 dedths2 38567 bnd2d 48298 |
Copyright terms: Public domain | W3C validator |