![]() |
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 414 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 52 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: sylancb 601 sylancbr 602 eqeq12d 2754 rru 3736 dedth2v 4547 dedth3v 4548 dedth4v 4549 disjprsn 4674 opidg 4848 unisng 4885 intsng 4945 isso2i 5578 poinxp 5709 posn 5714 xpid11 5884 dfpo2 6245 predpoirr 6284 predfrirr 6285 f1oprswap 6824 f1o2sn 7083 residpr 7084 f1mpt 7203 f1eqcocnv 7242 f1eqcocnvOLD 7243 isopolem 7285 3xpexg 7677 sqxpexg 7680 poxp 8049 oe0 8436 oecl 8451 nnmsucr 8540 ecopover 8694 enrefg 8858 php 9088 phpOLD 9100 3xpfi 9197 dffi3 9301 infxpenlem 9883 isfin5 10169 isfin5-2 10261 fpwwe2lem4 10504 pwfseqlem4a 10531 pwfseqlem4 10532 pwfseqlem5 10533 pwfseq 10534 nqereu 10799 halfnq 10846 ltsopr 10902 1idsr 10968 00sr 10969 sqgt0sr 10976 leid 11185 msqgt0 11609 msqge0 11610 recextlem1 11719 recextlem2 11720 recex 11721 div1 11778 cju 12083 2halves 12315 msqznn 12519 xrltnr 12970 xrleid 13000 iccid 13239 m1expeven 13945 sqneg 13951 sqcl 13953 nnsqcl 13962 qsqcl 13964 expubnd 14010 bernneq 14059 faclbnd 14119 faclbnd3 14121 hashfac 14286 leiso 14287 cjmulval 14965 fallrisefac 15844 sin2t 15995 cos2t 15996 divalglem0 16211 divalglem2 16213 gcd0id 16335 lcmid 16421 lcmgcdeq 16424 lcmfsn 16447 isprm5 16519 prslem 18123 pslem 18397 dirref 18426 efmndbasabf 18618 efmndhash 18622 efmndbasfi 18623 efmnd1bas 18639 submefmnd 18641 sgrp2nmndlem4 18674 grpsubid 18766 grp1inv 18790 cntzi 19044 permsetexOLD 19086 symgbasfi 19095 symg1bas 19107 pgrpsubgsymg 19126 symgextfve 19136 pmtrfinv 19178 psgnsn 19237 ringadd2 19926 ipeq0 20971 matsca2 21697 matbas2 21698 matplusgcell 21710 matsubgcell 21711 mamulid 21718 mamurid 21719 mattposcl 21730 mat1dimelbas 21748 mat1dimscm 21752 mat1dimmul 21753 m1detdiag 21874 mdetdiagid 21877 mdetunilem9 21897 pmatcoe1fsupp 21978 d1mat2pmat 22016 idcn 22536 hausdiag 22924 symgtgp 23385 ustref 23498 ustelimasn 23502 iducn 23563 ismet 23604 isxmet 23605 idnghm 24035 resubmet 24093 xrsxmet 24100 cphnm 24485 tcphnmval 24521 ipcau2 24526 tcphcphlem1 24527 tcphcphlem2 24528 tcphcph 24529 cmssmscld 24642 chordthmlem 26110 slerflex 27039 ismot 27282 hmoval 29557 htth 29665 hvsubid 29773 hvnegid 29774 hv2times 29808 hiidrcl 29842 normval 29871 issh2 29956 chjidm 30267 normcan 30323 ho2times 30566 kbpj 30703 lnop0 30713 riesz3i 30809 leoprf 30875 leopsq 30876 cvnref 31038 gtiso 31416 fldextid 32138 prsss 32277 deranglem 33540 poxp2 34182 poxp3 34188 lrrecpo 34249 subsid 34339 elfix2 34420 linedegen 34659 filnetlem2 34782 bj-ru0 35344 matunitlindflem2 36006 matunitlindf 36007 ftc1anclem3 36084 prdsbnd2 36185 reheibor 36229 ismgmOLD 36240 opidon2OLD 36244 exidreslem 36267 rngo2 36297 opideq 36735 eldmcoss2 36852 2xp3dxp2ge1d 40545 sn-inelr 40836 mzpf 40961 acongrep 41206 ttac 41262 mendval 41412 iocinico 41448 iocmbl 41449 seff 42390 sblpnf 42391 sigarid 44890 cnambpcma 45317 2leaddle2 45321 clintopval 45929 2arymaptfv 46528 2arymaptfo 46531 itcoval2 46541 itcoval3 46542 |
Copyright terms: Public domain | W3C validator |