|   | 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 1420 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 | 
| 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 1088 | 
| This theorem is referenced by: npncan2 11537 ltsubpos 11756 leaddle0 11779 subge02 11780 halfaddsub 12501 avglt1 12506 hashssdif 14452 pythagtriplem4 16858 pythagtriplem14 16867 lsmss2 19686 grpoidinvlem2 30525 hvpncan3 31062 bcm1n 32798 revpfxsfxrev 35122 nnproddivdvdsd 42002 resubidaddlid 42430 reposdif 42478 3anidm12p1 44831 3impcombi 44842 | 
| Copyright terms: Public domain | W3C validator |