| 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 1119 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒) |
| 3 | 2 | anabss3 675 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: supsn 9512 infsn 9545 grusn 10844 subeq0 11535 halfaddsub 12499 avglt2 12505 modabs2 13945 efsub 16136 sinmul 16208 divalgmod 16443 modgcd 16569 pythagtriplem4 16857 pythagtriplem16 16868 pltirr 18380 latjidm 18507 latmidm 18519 ipopos 18581 mulgmodid 19131 f1omvdcnv 19462 lsmss1 19683 rhmsubclem3 20687 zntoslem 21575 obsipid 21742 smadiadetlem2 22670 smadiadet 22676 ordtt1 23387 xmet0 24352 nmsq 25228 tcphcphlem3 25267 tcphcph 25271 grpoidinvlem1 30523 grpodivid 30561 nvmid 30678 ipidsq 30729 5oalem1 31673 3oalem2 31682 unopf1o 31935 unopnorm 31936 hmopre 31942 ballotlemfc0 34495 ballotlemfcc 34496 gcdabsorb 35750 cgr3rflx 36055 endofsegid 36086 tailini 36377 nnssi2 36456 nndivlub 36459 brin2 38410 opoccl 39195 opococ 39196 opexmid 39208 opnoncon 39209 cmtidN 39258 ltrniotaidvalN 40585 pell14qrexpclnn0 42877 rmxdbl 42951 rmydbl 42952 rhmsubcALTVlem3 48199 |
| Copyright terms: Public domain | W3C validator |