Theorem 3anidm13 1420

Description: Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)

Hypothesis

Ref	Expression
3anidm13.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒)

Assertion

Ref	Expression
3anidm13	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem 3anidm13

Step	Hyp	Ref	Expression
1		3anidm13.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒)
2	1	3com23 1126	. 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)
3	2	3anidm12 1419	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

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:  npncan2  11563  ltsubpos  11782  leaddle0  11805  subge02  11806  halfaddsub  12526  avglt1  12531  hashssdif  14461  pythagtriplem4  16866  pythagtriplem14  16875  lsmss2  19709  grpoidinvlem2  30537  hvpncan3  31074  bcm1n  32800  revpfxsfxrev  35083  nnproddivdvdsd  41957  resubidaddlid  42371  reposdif  42419  3anidm12p1  44777  3impcombi  44788