![]() |
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 113 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 48 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 106 |
This theorem is referenced by: sylancb 409 sylancbr 410 intsng 3678 pwnss 3941 posng 4438 xpid11m 4585 resiexg 4683 f1mpt 5442 f1eqcocnv 5462 isopolem 5492 poxp 5884 nnmsucr 6132 erex 6196 ecopover 6270 ecopoverg 6273 enrefg 6311 ltsopi 6572 recexnq 6642 ltsonq 6650 ltaddnq 6659 nsmallnqq 6664 ltpopr 6847 ltposr 7002 1idsr 7007 00sr 7008 axltirr 7246 leid 7262 reapirr 7744 inelr 7751 apsqgt0 7768 apirr 7772 msqge0 7783 recextlem1 7808 recexaplem2 7809 recexap 7810 div1 7858 cju 8105 2halves 8327 msqznn 8528 xrltnr 8931 xrleid 8950 iooidg 9008 iccid 9024 m1expeven 9620 expubnd 9630 sqneg 9632 sqcl 9634 sqap0 9639 nnsqcl 9642 qsqcl 9644 subsq2 9679 bernneq 9690 faclbnd 9765 faclbnd3 9767 cjmulval 9913 gcd0id 10514 lcmid 10606 lcmgcdeq 10609 bj-snexg 10861 |
Copyright terms: Public domain | W3C validator |