![]() |
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 115 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 49 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: sylancb 418 sylancbr 419 intsng 3904 pwnss 4188 posng 4731 sqxpexg 4775 xpid11 4885 resiexg 4987 f1mpt 5814 f1eqcocnv 5834 isopolem 5865 poxp 6285 nnmsucr 6541 erex 6611 ecopover 6687 ecopoverg 6690 enrefg 6818 3xpfi 6987 tapeq2 7313 netap 7314 2omotaplemap 7317 ltsopi 7380 recexnq 7450 ltsonq 7458 ltaddnq 7467 nsmallnqq 7472 ltpopr 7655 ltposr 7823 1idsr 7828 00sr 7829 axltirr 8086 leid 8103 reapirr 8596 inelr 8603 apsqgt0 8620 apirr 8624 msqge0 8635 recextlem1 8670 recexaplem2 8671 recexap 8672 div1 8722 cju 8980 2halves 9211 msqznn 9417 xrltnr 9845 xrleid 9866 iooidg 9975 iccid 9991 m1expeven 10657 expubnd 10667 sqneg 10669 sqcl 10671 sqap0 10677 nnsqcl 10680 qsqcl 10682 subsq2 10718 bernneq 10731 faclbnd 10812 faclbnd3 10814 cjmulval 11032 sin2t 11892 cos2t 11893 gcd0id 12116 lcmid 12218 lcmgcdeq 12221 intopsn 12950 mgm1 12953 sgrp1 12994 mnd1 13027 mnd1id 13028 grpsubid 13156 grp1 13178 grp1inv 13179 ringadd2 13523 ring1 13555 idcn 14380 ismet 14512 isxmet 14513 resubmet 14716 bj-snexg 15404 |
Copyright terms: Public domain | W3C validator |