![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anidms | Structured version Visualization version 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 449 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 52 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 |
This theorem is referenced by: sylancb 700 sylancbr 701 dedth2v 4176 dedth3v 4177 dedth4v 4178 disjprsn 4282 opidg 4452 intsng 4544 pwnss 4860 snex 4938 isso2i 5096 poinxp 5216 posn 5221 xpid11 5379 predpoirr 5746 predfrirr 5747 f1oprswap 6218 f1o2sn 6448 residpr 6449 f1mpt 6558 f1eqcocnv 6596 isopolem 6635 3xpexg 7003 sqxpexg 7005 poxp 7334 oe0 7647 oecl 7662 nnmsucr 7750 ecopover 7894 enrefg 8029 php 8185 3xpfi 8273 dffi3 8378 infxpenlem 8874 xp2cda 9040 isfin5-2 9251 fpwwe2lem5 9494 pwfseqlem4a 9521 pwfseqlem4 9522 pwfseqlem5 9523 pwfseq 9524 nqereu 9789 halfnq 9836 ltsopr 9892 1idsr 9957 00sr 9958 sqgt0sr 9965 leid 10171 msqgt0 10586 msqge0 10587 recextlem1 10695 recextlem2 10696 recex 10697 div1 10754 cju 11054 2halves 11298 msqznn 11497 xrltnr 11991 xrleid 12021 iccid 12258 m1expeven 12947 expubnd 12961 sqneg 12963 sqcl 12965 nnsqcl 12973 qsqcl 12975 subsq2 13013 bernneq 13030 faclbnd 13117 faclbnd3 13119 hashfac 13280 leiso 13281 cjmulval 13929 fallrisefac 14800 sin2t 14951 cos2t 14952 divalglem0 15163 divalglem2 15165 gcd0id 15287 lcmid 15369 lcmgcdeq 15372 lcmfsn 15395 isprm5 15466 prslem 16978 pslem 17253 dirref 17282 sgrp2nmndlem4 17462 grpsubid 17546 grp1inv 17570 cntzi 17808 symgval 17845 symgbas 17846 symgbasfi 17852 symg1bas 17862 pgrpsubgsymg 17874 symgextfve 17885 pmtrfinv 17927 psgnsn 17986 lsmidm 18123 ringadd2 18621 ipeq0 20031 matsca2 20274 matbas2 20275 matplusgcell 20287 matsubgcell 20288 mamulid 20295 mamurid 20296 mattposcl 20307 mat1dimelbas 20325 mat1dimscm 20329 mat1dimmul 20330 m1detdiag 20451 mdetdiagid 20454 mdetunilem9 20474 pmatcoe1fsupp 20554 d1mat2pmat 20592 idcn 21109 hausdiag 21496 symgtgp 21952 ustref 22069 ustelimasn 22073 iducn 22134 ismet 22175 isxmet 22176 idnghm 22594 resubmet 22652 xrsxmet 22659 cphnm 23039 tchnmval 23074 ipcau2 23079 tchcphlem1 23080 tchcphlem2 23081 tchcph 23082 chordthmlem 24604 ismot 25475 hmoval 27793 htth 27903 hvsubid 28011 hvnegid 28012 hv2times 28046 hiidrcl 28080 normval 28109 issh2 28194 chjidm 28507 normcan 28563 ho2times 28806 kbpj 28943 lnop0 28953 riesz3i 29049 leoprf 29115 leopsq 29116 cvnref 29278 gtiso 29606 prsss 30090 deranglem 31274 dfpo2 31771 elfix2 32136 linedegen 32375 filnetlem2 32499 bj-ru0 33057 matunitlindflem2 33536 matunitlindf 33537 ftc1anclem3 33617 prdsbnd2 33724 reheibor 33768 ismgmOLD 33779 opidon2OLD 33783 exidreslem 33806 rngo2 33836 opideq 34250 eldmcoss2 34349 mzpf 37616 acongrep 37864 ttac 37920 mendval 38070 mendplusgfval 38072 mendmulrfval 38074 iocinico 38114 iocmbl 38115 seff 38825 sblpnf 38826 sigarid 41368 cnambpcma 41634 2leaddle2 41637 clintopval 42165 |
Copyright terms: Public domain | W3C validator |