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 1263 | . 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒) |
3 | 2 | 3anidm12 1375 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: npncan2 10187 ltsubpos 10399 leaddle0 10422 subge02 10423 halfaddsub 11142 avglt1 11147 hashssdif 13061 pythagtriplem4 15362 pythagtriplem14 15371 lsmss2 17904 grpoidinvlem2 26743 hvpncan3 27283 bcm1n 28941 fv1stcnv 30925 sltasym 31071 3anidm12p1 38054 3impcombi 38065 |
Copyright terms: Public domain | W3C validator |