Theorem 3anidm13 1447

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 1144	. 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)
3	2	3anidm12 1446	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  npncan2  11585  ltsubpos  11808  leaddle0  11831  subge02  11832  halfaddsub  12579  avglt1  12584  hashssdif  14557  revpfxsfxrev  14917  pythagtriplem4  16997  pythagtriplem14  17006  lsmss2  19881  grpoidinvlem2  31107  hvpncan3  31644  bcm1n  33387  nnproddivdvdsd  43051  resubidaddlid  43447  reposdif  43520  3anidm12p1  45788  3impcombi  45799