| 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 4591. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4597 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4597. (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 4531 | . . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
| 3 | 2 | eqcomd 2743 | . . 3 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
| 4 | dedth.1 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒)) | |
| 5 | 3, 4 | syl 17 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| 6 | 1, 5 | mpbiri 258 | 1 ⊢ (𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ifcif 4525 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-if 4526 |
| This theorem is referenced by: dedth2h 4585 dedth3h 4586 orduninsuc 7864 oeoe 8637 limensuc 9194 axcc4dom 10481 inar1 10815 supsr 11152 renegcl 11572 peano5uzti 12708 uzenom 14005 seqfn 14054 seq1 14055 seqp1 14057 hashxp 14473 smadiadetr 22681 imsmet 30710 smcn 30717 nmlno0i 30813 nmblolbi 30819 blocn 30826 dipdir 30861 dipass 30864 siilem2 30871 htth 30937 normlem6 31134 normlem7tALT 31138 normsq 31153 hhssablo 31282 hhssnvt 31284 hhsssh 31288 shintcl 31349 chintcl 31351 pjhth 31412 ococ 31425 chm0 31510 chne0 31513 chocin 31514 chj0 31516 chjo 31534 h1de2ci 31575 spansn 31578 elspansn 31585 pjch1 31689 pjinormi 31706 pjige0 31710 hoaddrid 31810 hodid 31811 nmlnop0 32017 lnopunilem2 32030 elunop2 32032 lnophm 32038 nmbdoplb 32044 nmcopex 32048 nmcoplb 32049 lnopcon 32054 lnfn0 32066 lnfnmul 32067 nmbdfnlb 32069 nmcfnex 32072 nmcfnlb 32073 lnfncon 32075 riesz4 32083 riesz1 32084 cnlnadjeu 32097 pjhmop 32169 hmopidmch 32172 hmopidmpj 32173 pjss2coi 32183 pjssmi 32184 pjssge0i 32185 pjdifnormi 32186 pjidmco 32200 mdslmd1lem3 32346 mdslmd1lem4 32347 csmdsymi 32353 hatomic 32379 atord 32407 atcvat2 32408 chirred 32414 bnj941 34786 bnj944 34952 sqdivzi 35728 onsucconn 36439 onsucsuccmp 36445 limsucncmp 36447 dedths 38963 dedths2 38966 bnd2d 49200 |
| Copyright terms: Public domain | W3C validator |