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  11556  ltsubpos  11777  leaddle0  11800  subge02  11801  halfaddsub  12548  avglt1  12553  hashssdif  14524  revpfxsfxrev  14884  pythagtriplem4  16958  pythagtriplem14  16967  lsmss2  19842  grpoidinvlem2  31040  hvpncan3  31577  bcm1n  33320  nnproddivdvdsd  42970  resubidaddlid  43374  reposdif  43447  3anidm12p1  45732  3impcombi  45743