![]() |
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 2749 rru 3741 dedth2v 4552 dedth3v 4553 dedth4v 4554 disjprsn 4679 opidg 4853 unisng 4890 intsng 4950 isso2i 5584 poinxp 5716 posn 5721 xpid11 5891 dfpo2 6252 predpoirr 6291 predfrirr 6292 f1oprswap 6832 f1o2sn 7092 residpr 7093 f1mpt 7212 f1eqcocnv 7251 f1eqcocnvOLD 7252 isopolem 7294 3xpexg 7690 sqxpexg 7693 poxp 8064 poxp2 8079 poxp3 8086 oe0 8472 oecl 8487 nnmsucr 8576 ecopover 8766 enrefg 8930 php 9160 phpOLD 9172 3xpfi 9269 dffi3 9375 infxpenlem 9957 isfin5 10243 isfin5-2 10335 fpwwe2lem4 10578 pwfseqlem4a 10605 pwfseqlem4 10606 pwfseqlem5 10607 pwfseq 10608 nqereu 10873 halfnq 10920 ltsopr 10976 1idsr 11042 00sr 11043 sqgt0sr 11050 leid 11259 msqgt0 11683 msqge0 11684 recextlem1 11793 recextlem2 11794 recex 11795 div1 11852 cju 12157 2halves 12389 msqznn 12593 xrltnr 13048 xrleid 13079 iccid 13318 m1expeven 14024 sqneg 14030 sqcl 14032 nnsqcl 14042 qsqcl 14044 expubnd 14091 bernneq 14141 faclbnd 14199 faclbnd3 14201 hashfac 14366 leiso 14367 cjmulval 15039 fallrisefac 15916 sin2t 16067 cos2t 16068 divalglem0 16283 divalglem2 16285 gcd0id 16407 lcmid 16493 lcmgcdeq 16496 lcmfsn 16519 isprm5 16591 prslem 18195 pslem 18469 dirref 18498 efmndbasabf 18690 efmndhash 18694 efmndbasfi 18695 efmnd1bas 18711 submefmnd 18713 sgrp2nmndlem4 18746 grpsubid 18839 grp1inv 18863 cntzi 19117 permsetexOLD 19159 symgbasfi 19168 symg1bas 19180 pgrpsubgsymg 19199 symgextfve 19209 pmtrfinv 19251 psgnsn 19310 ipeq0 21065 matsca2 21792 matbas2 21793 matplusgcell 21805 matsubgcell 21806 mamulid 21813 mamurid 21814 mattposcl 21825 mat1dimelbas 21843 mat1dimscm 21847 mat1dimmul 21848 m1detdiag 21969 mdetdiagid 21972 mdetunilem9 21992 pmatcoe1fsupp 22073 d1mat2pmat 22111 idcn 22631 hausdiag 23019 symgtgp 23480 ustref 23593 ustelimasn 23597 iducn 23658 ismet 23699 isxmet 23700 idnghm 24130 resubmet 24188 xrsxmet 24195 cphnm 24580 tcphnmval 24616 ipcau2 24621 tcphcphlem1 24622 tcphcphlem2 24623 tcphcph 24624 cmssmscld 24737 chordthmlem 26205 slerflex 27134 lrrecpo 27282 subsid 27385 ismot 27526 hmoval 29801 htth 29909 hvsubid 30017 hvnegid 30018 hv2times 30052 hiidrcl 30086 normval 30115 issh2 30200 chjidm 30511 normcan 30567 ho2times 30810 kbpj 30947 lnop0 30957 riesz3i 31053 leoprf 31119 leopsq 31120 cvnref 31282 gtiso 31668 fldextid 32412 prsss 32561 deranglem 33824 elfix2 34542 linedegen 34781 filnetlem2 34904 bj-ru0 35463 matunitlindflem2 36125 matunitlindf 36126 ftc1anclem3 36203 prdsbnd2 36304 reheibor 36348 ismgmOLD 36359 opidon2OLD 36363 exidreslem 36386 rngo2 36416 opideq 36854 eldmcoss2 36971 2xp3dxp2ge1d 40664 sn-inelr 40981 mzpf 41106 acongrep 41351 ttac 41407 mendval 41557 iocinico 41593 iocmbl 41594 seff 42681 sblpnf 42682 sigarid 45189 cnambpcma 45616 2leaddle2 45620 clintopval 46228 2arymaptfv 46827 2arymaptfo 46830 itcoval2 46840 itcoval3 46841 |
Copyright terms: Public domain | W3C validator |