![]() |
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 413 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 52 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: sylancb 599 sylancbr 600 rru 3704 dedth2v 4441 dedth3v 4442 dedth4v 4443 disjprsn 4557 opidg 4729 unisng 4760 intsng 4817 snex 5223 isso2i 5396 poinxp 5518 posn 5523 xpid11 5684 predpoirr 6051 predfrirr 6052 f1oprswap 6526 f1o2sn 6767 residpr 6768 f1mpt 6884 f1eqcocnv 6922 isopolem 6961 3xpexg 7332 sqxpexg 7334 poxp 7675 oe0 7998 oecl 8013 nnmsucr 8101 ecopover 8251 enrefg 8389 php 8548 3xpfi 8636 dffi3 8741 infxpenlem 9285 isfin5 9567 isfin5-2 9659 fpwwe2lem5 9902 pwfseqlem4a 9929 pwfseqlem4 9930 pwfseqlem5 9931 pwfseq 9932 nqereu 10197 halfnq 10244 ltsopr 10300 1idsr 10366 00sr 10367 sqgt0sr 10374 leid 10583 msqgt0 11008 msqge0 11009 recextlem1 11118 recextlem2 11119 recex 11120 div1 11177 cju 11482 2halves 11713 msqznn 11913 xrltnr 12364 xrleid 12394 iccid 12633 m1expeven 13326 sqneg 13332 sqcl 13334 nnsqcl 13343 qsqcl 13345 expubnd 13391 bernneq 13440 faclbnd 13500 faclbnd3 13502 hashfac 13664 leiso 13665 cjmulval 14338 fallrisefac 15212 sin2t 15363 cos2t 15364 divalglem0 15577 divalglem2 15579 gcd0id 15700 lcmid 15782 lcmgcdeq 15785 lcmfsn 15808 isprm5 15880 prslem 17370 pslem 17645 dirref 17674 sgrp2nmndlem4 17854 grpsubid 17940 grp1inv 17964 cntzi 18200 symgval 18238 symgbas 18239 symgbasfi 18245 symg1bas 18255 pgrpsubgsymg 18267 symgextfve 18278 pmtrfinv 18320 psgnsn 18379 lsmidm 18517 ringadd2 19015 ipeq0 20464 matsca2 20713 matbas2 20714 matplusgcell 20726 matsubgcell 20727 mamulid 20734 mamurid 20735 mattposcl 20746 mat1dimelbas 20764 mat1dimscm 20768 mat1dimmul 20769 m1detdiag 20890 mdetdiagid 20893 mdetunilem9 20913 pmatcoe1fsupp 20993 d1mat2pmat 21031 idcn 21549 hausdiag 21937 symgtgp 22393 ustref 22510 ustelimasn 22514 iducn 22575 ismet 22616 isxmet 22617 idnghm 23035 resubmet 23093 xrsxmet 23100 cphnm 23480 tcphnmval 23515 ipcau2 23520 tcphcphlem1 23521 tcphcphlem2 23522 tcphcph 23523 cmssmscld 23636 chordthmlem 25091 ismot 26003 hmoval 28278 htth 28386 hvsubid 28494 hvnegid 28495 hv2times 28529 hiidrcl 28563 normval 28592 issh2 28677 chjidm 28988 normcan 29044 ho2times 29287 kbpj 29424 lnop0 29434 riesz3i 29530 leoprf 29596 leopsq 29597 cvnref 29759 gtiso 30124 fldextid 30653 prsss 30776 deranglem 32021 dfpo2 32599 elfix2 32974 linedegen 33213 filnetlem2 33336 bj-ru0 33824 matunitlindflem2 34420 matunitlindf 34421 ftc1anclem3 34500 prdsbnd2 34605 reheibor 34649 ismgmOLD 34660 opidon2OLD 34664 exidreslem 34687 rngo2 34717 opideq 35132 eldmcoss2 35230 mzpf 38818 acongrep 39062 ttac 39118 mendval 39268 mendplusgfval 39270 mendmulrfval 39272 iocinico 39303 iocmbl 39304 seff 40179 sblpnf 40180 sigarid 42657 cnambpcma 43010 2leaddle2 43014 clintopval 43589 |
Copyright terms: Public domain | W3C validator |