![]() |
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 411 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 52 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: sylancb 598 sylancbr 599 eqeq12d 2741 rru 3772 dedth2v 4594 dedth3v 4595 dedth4v 4596 disjprsn 4722 opidg 4897 unisng 4932 intsng 4992 isso2i 5628 poinxp 5761 posn 5766 xpid11 5937 dfpo2 6306 predpoirr 6345 predfrirr 6346 f1oprswap 6886 f1o2sn 7155 residpr 7156 f1mpt 7275 f1eqcocnv 7314 isopolem 7356 3xpexg 7759 sqxpexg 7762 poxp 8141 poxp2 8156 poxp3 8163 oe0 8551 oecl 8566 nnmsucr 8654 ecopover 8849 enrefg 9014 php 9247 phpOLD 9259 3xpfi 9357 dffi3 9470 infxpenlem 10052 isfin5 10338 isfin5-2 10430 fpwwe2lem4 10673 pwfseqlem4a 10700 pwfseqlem4 10701 pwfseqlem5 10702 pwfseq 10703 nqereu 10968 halfnq 11015 ltsopr 11071 1idsr 11137 00sr 11138 sqgt0sr 11145 leid 11356 msqgt0 11780 msqge0 11781 recextlem1 11890 recextlem2 11891 recex 11892 div1 11950 cju 12255 2halves 12487 msqznn 12691 xrltnr 13148 xrleid 13179 iccid 13418 m1expeven 14124 sqneg 14130 sqcl 14132 nnsqcl 14142 qsqcl 14144 expubnd 14191 bernneq 14241 faclbnd 14302 faclbnd3 14304 hashfac 14472 leiso 14473 cjmulval 15145 fallrisefac 16022 sin2t 16174 cos2t 16175 divalglem0 16390 divalglem2 16392 gcd0id 16514 lcmid 16605 lcmgcdeq 16608 lcmfsn 16631 isprm5 16703 prslem 18318 pslem 18592 dirref 18621 efmndbasabf 18857 efmndhash 18861 efmndbasfi 18862 efmnd1bas 18878 submefmnd 18880 sgrp2nmndlem4 18913 grpsubid 19013 grp1inv 19037 cntzi 19318 permsetexOLD 19362 symgbasfi 19371 symg1bas 19383 pgrpsubgsymg 19402 symgextfve 19412 pmtrfinv 19454 psgnsn 19513 ipeq0 21626 matsca2 22405 matbas2 22406 matplusgcell 22418 matsubgcell 22419 mamulid 22426 mamurid 22427 mattposcl 22438 mat1dimelbas 22456 mat1dimscm 22460 mat1dimmul 22461 m1detdiag 22582 mdetdiagid 22585 mdetunilem9 22605 pmatcoe1fsupp 22686 d1mat2pmat 22724 idcn 23244 hausdiag 23632 symgtgp 24093 ustref 24206 ustelimasn 24210 iducn 24271 ismet 24312 isxmet 24313 idnghm 24743 resubmet 24801 xrsxmet 24808 cphnm 25204 tcphnmval 25240 ipcau2 25245 tcphcphlem1 25246 tcphcphlem2 25247 tcphcph 25248 cmssmscld 25361 chordthmlem 26852 slerflex 27785 lrrecpo 27947 subsid 28068 divs1 28196 ismot 28454 hmoval 30735 htth 30843 hvsubid 30951 hvnegid 30952 hv2times 30986 hiidrcl 31020 normval 31049 issh2 31134 chjidm 31445 normcan 31501 ho2times 31744 kbpj 31881 lnop0 31891 riesz3i 31987 leoprf 32053 leopsq 32054 cvnref 32216 gtiso 32603 fldextid 33520 prsss 33687 deranglem 34946 elfix2 35676 linedegen 35915 filnetlem2 36039 bj-ru0 36597 matunitlindflem2 37266 matunitlindf 37267 ftc1anclem3 37344 prdsbnd2 37444 reheibor 37488 ismgmOLD 37499 opidon2OLD 37503 exidreslem 37526 rngo2 37556 opideq 37989 eldmcoss2 38105 2xp3dxp2ge1d 41870 sn-inelr 42187 mzpf 42330 acongrep 42575 ttac 42631 mendval 42781 iocinico 42814 iocmbl 42815 seff 43920 sblpnf 43921 sigarid 46416 cnambpcma 46844 2leaddle2 46848 grlicref 47439 clintopval 47518 2arymaptfv 47976 2arymaptfo 47979 itcoval2 47989 itcoval3 47990 |
Copyright terms: Public domain | W3C validator |