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 1128 | . 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒) |
3 | 2 | 3anidm12 1421 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: npncan2 11102 ltsubpos 11321 leaddle0 11344 subge02 11345 halfaddsub 12060 avglt1 12065 hashssdif 13976 pythagtriplem4 16369 pythagtriplem14 16378 lsmss2 19054 grpoidinvlem2 28583 hvpncan3 29120 bcm1n 30833 revpfxsfxrev 32787 nnproddivdvdsd 39741 resubidaddid1 40084 reposdif 40130 3anidm12p1 42097 3impcombi 42108 |
Copyright terms: Public domain | W3C validator |