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 108 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 43 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 |
This theorem is referenced by: sylancb 395 sylancbr 396 intsng 3649 pwnss 3912 posng 4412 xpid11m 4557 resiexg 4653 f1mpt 5410 f1eqcocnv 5431 isopolem 5461 poxp 5853 nnmsucr 6067 erex 6130 ecopover 6204 ecopoverg 6207 enrefg 6244 ltsopi 6418 recexnq 6488 ltsonq 6496 ltaddnq 6505 nsmallnqq 6510 ltpopr 6693 ltposr 6848 1idsr 6853 00sr 6854 axltirr 7086 leid 7102 reapirr 7568 inelr 7575 apsqgt0 7592 apirr 7596 msqge0 7607 recextlem1 7632 recexaplem2 7633 recexap 7634 div1 7680 cju 7913 2halves 8154 msqznn 8338 xrltnr 8701 xrleid 8720 iooidg 8778 iccid 8794 expubnd 9311 sqneg 9313 sqcl 9315 sqap0 9320 nnsqcl 9323 qsqcl 9325 subsq2 9359 bernneq 9369 cjmulval 9488 bj-snexg 10032 |
Copyright terms: Public domain | W3C validator |