![]() |
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 4438. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4444 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4444. (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 4381 | . . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2799 | . . 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 1520 ifcif 4375 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-ex 1760 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-if 4376 |
This theorem is referenced by: dedth2h 4432 dedth3h 4433 orduninsuc 7405 oeoe 8066 limensuc 8531 axcc4dom 9698 inar1 10032 supsr 10369 renegcl 10786 peano5uzti 11910 uzenom 13170 seqfn 13219 seq1 13220 seqp1 13222 hashxp 13631 smadiadetr 20956 imsmet 28147 smcn 28154 nmlno0i 28250 nmblolbi 28256 blocn 28263 dipdir 28298 dipass 28301 siilem2 28308 htth 28374 normlem6 28571 normlem7tALT 28575 normsq 28590 hhssablo 28719 hhssnvt 28721 hhsssh 28725 shintcl 28786 chintcl 28788 pjhth 28849 ococ 28862 chm0 28947 chne0 28950 chocin 28951 chj0 28953 chjo 28971 h1de2ci 29012 spansn 29015 elspansn 29022 pjch1 29126 pjinormi 29143 pjige0 29147 hoaddid1 29247 hodid 29248 nmlnop0 29454 lnopunilem2 29467 elunop2 29469 lnophm 29475 nmbdoplb 29481 nmcopex 29485 nmcoplb 29486 lnopcon 29491 lnfn0 29503 lnfnmul 29504 nmbdfnlb 29506 nmcfnex 29509 nmcfnlb 29510 lnfncon 29512 riesz4 29520 riesz1 29521 cnlnadjeu 29534 pjhmop 29606 hmopidmch 29609 hmopidmpj 29610 pjss2coi 29620 pjssmi 29621 pjssge0i 29622 pjdifnormi 29623 pjidmco 29637 mdslmd1lem3 29783 mdslmd1lem4 29784 csmdsymi 29790 hatomic 29816 atord 29844 atcvat2 29845 chirred 29851 bnj941 31617 bnj944 31782 sqdivzi 32512 onsucconn 33339 onsucsuccmp 33345 limsucncmp 33347 dedths 35579 dedths2 35582 bnd2d 44218 |
Copyright terms: Public domain | W3C validator |