| 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 412 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
| 3 | 2 | pm2.43i 52 | 1 ⊢ (𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: sylancb 600 sylancbr 601 ru0 2127 eqeq12d 2753 rru 3785 dedth2v 4588 dedth3v 4589 dedth4v 4590 disjprsn 4714 opidg 4892 unisng 4925 intsng 4983 isso2i 5629 poinxp 5766 posn 5771 xpid11 5943 dfpo2 6316 predpoirr 6354 predfrirr 6355 f1oprswap 6892 f1o2sn 7162 residpr 7163 f1mpt 7281 f1eqcocnv 7321 isopolem 7365 3xpexg 7772 sqxpexg 7775 poxp 8153 poxp2 8168 poxp3 8175 oe0 8560 oecl 8575 nnmsucr 8663 ecopover 8861 enrefg 9024 php 9247 phpOLD 9259 3xpfi 9360 dffi3 9471 infxpenlem 10053 isfin5 10339 isfin5-2 10431 pwfseqlem4a 10701 pwfseqlem4 10702 pwfseqlem5 10703 pwfseq 10704 nqereu 10969 halfnq 11016 ltsopr 11072 1idsr 11138 00sr 11139 sqgt0sr 11146 leid 11357 msqgt0 11783 msqge0 11784 recextlem1 11893 recextlem2 11894 recex 11895 div1 11957 cju 12262 2halves 12494 msqznn 12700 xrltnr 13161 xrleid 13193 iccid 13432 m1expeven 14150 sqneg 14156 sqcl 14158 nnsqcl 14168 qsqcl 14170 expubnd 14217 bernneq 14268 faclbnd 14329 faclbnd3 14331 hashfac 14497 leiso 14498 cjmulval 15184 fallrisefac 16061 sin2t 16213 cos2t 16214 divalglem0 16430 divalglem2 16432 gcd0id 16556 lcmid 16646 lcmgcdeq 16649 lcmfsn 16672 isprm5 16744 prslem 18343 pslem 18617 dirref 18646 efmndbasabf 18885 efmndhash 18889 efmndbasfi 18890 efmnd1bas 18906 submefmnd 18908 sgrp2nmndlem4 18941 grpsubid 19042 grp1inv 19066 cntzi 19347 symgbasfi 19396 symg1bas 19408 pgrpsubgsymg 19427 symgextfve 19437 pmtrfinv 19479 psgnsn 19538 ipeq0 21656 matsca2 22426 matbas2 22427 matplusgcell 22439 matsubgcell 22440 mamulid 22447 mamurid 22448 mattposcl 22459 mat1dimelbas 22477 mat1dimscm 22481 mat1dimmul 22482 m1detdiag 22603 mdetdiagid 22606 mdetunilem9 22626 pmatcoe1fsupp 22707 d1mat2pmat 22745 idcn 23265 hausdiag 23653 symgtgp 24114 ustref 24227 ustelimasn 24231 iducn 24292 ismet 24333 isxmet 24334 idnghm 24764 resubmet 24823 xrsxmet 24831 cphnm 25227 tcphnmval 25263 ipcau2 25268 tcphcphlem1 25269 tcphcphlem2 25270 tcphcph 25271 cmssmscld 25384 chordthmlem 26875 slerflex 27808 lrrecpo 27974 subsid 28099 divs1 28229 ismot 28543 hmoval 30829 htth 30937 hvsubid 31045 hvnegid 31046 hv2times 31080 hiidrcl 31114 normval 31143 issh2 31228 chjidm 31539 normcan 31595 ho2times 31838 kbpj 31975 lnop0 31985 riesz3i 32081 leoprf 32147 leopsq 32148 cvnref 32310 gtiso 32710 fldextid 33710 prsss 33915 deranglem 35171 elfix2 35905 linedegen 36144 filnetlem2 36380 matunitlindflem2 37624 matunitlindf 37625 ftc1anclem3 37702 prdsbnd2 37802 reheibor 37846 ismgmOLD 37857 opidon2OLD 37861 exidreslem 37884 rngo2 37914 opideq 38344 eldmcoss2 38460 2xp3dxp2ge1d 42242 sn-inelr 42497 mzpf 42747 acongrep 42992 ttac 43048 mendval 43191 iocinico 43224 iocmbl 43225 seff 44328 sblpnf 44329 sigarid 46873 cnambpcma 47306 2leaddle2 47310 grlicref 47972 clintopval 48120 2arymaptfv 48572 2arymaptfo 48575 itcoval2 48585 itcoval3 48586 |
| Copyright terms: Public domain | W3C validator |