Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anidms | GIF version |
Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.) |
Ref | Expression |
---|---|
anidms.1 | ⊢ ((𝜑 ∧ 𝜑) → 𝜓) |
Ref | Expression |
---|---|
anidms | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anidms.1 | . . 3 ⊢ ((𝜑 ∧ 𝜑) → 𝜓) | |
2 | 1 | ex 114 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 49 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: sylancb 414 sylancbr 415 intsng 3775 pwnss 4053 posng 4581 sqxpexg 4625 xpid11 4732 resiexg 4834 f1mpt 5640 f1eqcocnv 5660 isopolem 5691 poxp 6097 nnmsucr 6352 erex 6421 ecopover 6495 ecopoverg 6498 enrefg 6626 3xpfi 6787 ltsopi 7096 recexnq 7166 ltsonq 7174 ltaddnq 7183 nsmallnqq 7188 ltpopr 7371 ltposr 7539 1idsr 7544 00sr 7545 axltirr 7799 leid 7816 reapirr 8307 inelr 8314 apsqgt0 8331 apirr 8335 msqge0 8346 recextlem1 8380 recexaplem2 8381 recexap 8382 div1 8431 cju 8687 2halves 8917 msqznn 9119 xrltnr 9534 xrleid 9554 iooidg 9660 iccid 9676 m1expeven 10308 expubnd 10318 sqneg 10320 sqcl 10322 sqap0 10327 nnsqcl 10330 qsqcl 10332 subsq2 10368 bernneq 10380 faclbnd 10455 faclbnd3 10457 cjmulval 10628 sin2t 11383 cos2t 11384 gcd0id 11594 lcmid 11688 lcmgcdeq 11691 idcn 12308 ismet 12440 isxmet 12441 resubmet 12644 bj-snexg 13037 |
Copyright terms: Public domain | W3C validator |