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 3769 dedth2v 4525 dedth3v 4526 dedth4v 4527 disjprsn 4644 opidg 4816 unisng 4847 intsng 4904 snex 5323 isso2i 5502 poinxp 5626 posn 5631 xpid11 5796 predpoirr 6170 predfrirr 6171 f1oprswap 6652 f1o2sn 6897 residpr 6898 f1mpt 7010 f1eqcocnv 7048 isopolem 7087 3xpexg 7463 sqxpexg 7465 poxp 7813 oe0 8138 oecl 8153 nnmsucr 8241 ecopover 8391 enrefg 8530 php 8690 3xpfi 8779 dffi3 8884 infxpenlem 9428 isfin5 9710 isfin5-2 9802 fpwwe2lem5 10045 pwfseqlem4a 10072 pwfseqlem4 10073 pwfseqlem5 10074 pwfseq 10075 nqereu 10340 halfnq 10387 ltsopr 10443 1idsr 10509 00sr 10510 sqgt0sr 10517 leid 10725 msqgt0 11149 msqge0 11150 recextlem1 11259 recextlem2 11260 recex 11261 div1 11318 cju 11623 2halves 11854 msqznn 12053 xrltnr 12504 xrleid 12534 iccid 12773 m1expeven 13466 sqneg 13472 sqcl 13474 nnsqcl 13483 qsqcl 13485 expubnd 13531 bernneq 13580 faclbnd 13640 faclbnd3 13642 hashfac 13806 leiso 13807 cjmulval 14494 fallrisefac 15369 sin2t 15520 cos2t 15521 divalglem0 15734 divalglem2 15736 gcd0id 15857 lcmid 15943 lcmgcdeq 15946 lcmfsn 15969 isprm5 16041 prslem 17531 pslem 17806 dirref 17835 sgrp2nmndlem4 18033 grpsubid 18123 grp1inv 18147 cntzi 18399 symgval 18437 symgbas 18438 symgbasfi 18444 symg1bas 18455 pgrpsubgsymg 18468 symgextfve 18478 pmtrfinv 18520 psgnsn 18579 lsmidmOLD 18720 ringadd2 19256 ipeq0 20712 matsca2 20959 matbas2 20960 matplusgcell 20972 matsubgcell 20973 mamulid 20980 mamurid 20981 mattposcl 20992 mat1dimelbas 21010 mat1dimscm 21014 mat1dimmul 21015 m1detdiag 21136 mdetdiagid 21139 mdetunilem9 21159 pmatcoe1fsupp 21239 d1mat2pmat 21277 idcn 21795 hausdiag 22183 symgtgp 22639 ustref 22756 ustelimasn 22760 iducn 22821 ismet 22862 isxmet 22863 idnghm 23281 resubmet 23339 xrsxmet 23346 cphnm 23726 tcphnmval 23761 ipcau2 23766 tcphcphlem1 23767 tcphcphlem2 23768 tcphcph 23769 cmssmscld 23882 chordthmlem 25337 ismot 26249 hmoval 28515 htth 28623 hvsubid 28731 hvnegid 28732 hv2times 28766 hiidrcl 28800 normval 28829 issh2 28914 chjidm 29225 normcan 29281 ho2times 29524 kbpj 29661 lnop0 29671 riesz3i 29767 leoprf 29833 leopsq 29834 cvnref 29996 gtiso 30363 fldextid 30949 prsss 31059 deranglem 32311 dfpo2 32889 elfix2 33263 linedegen 33502 filnetlem2 33625 bj-ru0 34151 matunitlindflem2 34771 matunitlindf 34772 ftc1anclem3 34851 prdsbnd2 34956 reheibor 35000 ismgmOLD 35011 opidon2OLD 35015 exidreslem 35038 rngo2 35068 opideq 35483 eldmcoss2 35581 mzpf 39213 acongrep 39457 ttac 39513 mendval 39663 iocinico 39698 iocmbl 39699 seff 40521 sblpnf 40522 sigarid 42996 cnambpcma 43375 2leaddle2 43379 efmndhash 43944 efmndbasfi 43945 efmnd1bas 43960 submefmnd 43962 clintopval 44009 |
Copyright terms: Public domain | W3C validator |