Theorem 3anidm13 1421

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 1420	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

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