![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anidm23 | Structured version Visualization version GIF version |
Description: Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.) |
Ref | Expression |
---|---|
3anidm23.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
3anidm23 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anidm23.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒) | |
2 | 1 | 3expa 1148 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒) |
3 | 2 | anabss3 666 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∧ w3a 1108 |
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 199 df-an 386 df-3an 1110 |
This theorem is referenced by: supsn 8620 infsn 8652 grusn 9914 subeq0 10599 halfaddsub 11553 avglt2 11559 modabs2 12959 efsub 15166 sinmul 15238 divalgmod 15465 modgcd 15588 pythagtriplem4 15857 pythagtriplem16 15868 pltirr 17278 latjidm 17389 latmidm 17401 ipopos 17475 mulgmodid 17894 f1omvdcnv 18176 lsmss1 18392 zntoslem 20226 obsipid 20391 smadiadetlem2 20797 smadiadet 20803 ordtt1 21512 xmet0 22475 nmsq 23321 tcphcphlem3 23359 tcphcph 23363 grpoidinvlem1 27884 grpodivid 27922 nvmid 28039 ipidsq 28090 5oalem1 29038 3oalem2 29047 unopf1o 29300 unopnorm 29301 hmopre 29307 ballotlemfc0 31071 ballotlemfcc 31072 pdivsq 32149 gcdabsorb 32152 cgr3rflx 32674 endofsegid 32705 tailini 32883 nnssi2 32962 nndivlub 32965 brin2 34661 opoccl 35215 opococ 35216 opexmid 35228 opnoncon 35229 cmtidN 35278 ltrniotaidvalN 36604 pell14qrexpclnn0 38216 rmxdbl 38289 rmydbl 38290 rhmsubclem3 42887 rhmsubcALTVlem3 42905 |
Copyright terms: Public domain | W3C validator |