![]() |
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 3876 pwnss 4156 posng 4695 sqxpexg 4739 xpid11 4846 resiexg 4948 f1mpt 5766 f1eqcocnv 5786 isopolem 5817 poxp 6227 nnmsucr 6483 erex 6553 ecopover 6627 ecopoverg 6630 enrefg 6758 3xpfi 6924 netap 7243 2omotaplemap 7246 ltsopi 7307 recexnq 7377 ltsonq 7385 ltaddnq 7394 nsmallnqq 7399 ltpopr 7582 ltposr 7750 1idsr 7755 00sr 7756 axltirr 8011 leid 8028 reapirr 8521 inelr 8528 apsqgt0 8545 apirr 8549 msqge0 8560 recextlem1 8594 recexaplem2 8595 recexap 8596 div1 8646 cju 8904 2halves 9134 msqznn 9339 xrltnr 9763 xrleid 9784 iooidg 9893 iccid 9909 m1expeven 10550 expubnd 10560 sqneg 10562 sqcl 10564 sqap0 10569 nnsqcl 10572 qsqcl 10574 subsq2 10610 bernneq 10623 faclbnd 10702 faclbnd3 10704 cjmulval 10878 sin2t 11738 cos2t 11739 gcd0id 11960 lcmid 12060 lcmgcdeq 12063 intopsn 12675 mgm1 12678 sgrp1 12705 mnd1 12734 mnd1id 12735 grpsubid 12840 grp1 12862 grp1inv 12863 ringadd2 13033 ring1 13059 idcn 13376 ismet 13508 isxmet 13509 resubmet 13712 bj-snexg 14317 |
Copyright terms: Public domain | W3C validator |