![]() |
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 1115 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒) |
3 | 2 | anabss3 673 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: supsn 9497 infsn 9530 grusn 10829 subeq0 11518 halfaddsub 12478 avglt2 12484 modabs2 13906 efsub 16080 sinmul 16152 divalgmod 16386 modgcd 16511 prmdvdssqOLD 16693 pythagtriplem4 16791 pythagtriplem16 16802 pltirr 18330 latjidm 18457 latmidm 18469 ipopos 18531 mulgmodid 19076 f1omvdcnv 19411 lsmss1 19632 rhmsubclem3 20632 zntoslem 21507 obsipid 21673 smadiadetlem2 22610 smadiadet 22616 ordtt1 23327 xmet0 24292 nmsq 25166 tcphcphlem3 25205 tcphcph 25209 grpoidinvlem1 30386 grpodivid 30424 nvmid 30541 ipidsq 30592 5oalem1 31536 3oalem2 31545 unopf1o 31798 unopnorm 31799 hmopre 31805 ballotlemfc0 34243 ballotlemfcc 34244 gcdabsorb 35475 cgr3rflx 35781 endofsegid 35812 tailini 35991 nnssi2 36070 nndivlub 36073 brin2 38011 opoccl 38796 opococ 38797 opexmid 38809 opnoncon 38810 cmtidN 38859 ltrniotaidvalN 40186 pell14qrexpclnn0 42428 rmxdbl 42502 rmydbl 42503 rhmsubcALTVlem3 47531 |
Copyright terms: Public domain | W3C validator |