![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anidm13 | Structured version Visualization version GIF version |
Description: Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.) |
Ref | Expression |
---|---|
3anidm13.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒) |
Ref | Expression |
---|---|
3anidm13 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anidm13.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒) | |
2 | 1 | 3com23 1126 | . 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒) |
3 | 2 | 3anidm12 1419 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: npncan2 11424 ltsubpos 11643 leaddle0 11666 subge02 11667 halfaddsub 12382 avglt1 12387 hashssdif 14304 pythagtriplem4 16683 pythagtriplem14 16692 lsmss2 19440 grpoidinvlem2 29333 hvpncan3 29870 bcm1n 31581 revpfxsfxrev 33578 nnproddivdvdsd 40425 resubidaddid1 40802 reposdif 40850 3anidm12p1 43030 3impcombi 43041 |
Copyright terms: Public domain | W3C validator |