Theorem 3anidm13 1446

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  npncan2  11491  ltsubpos  11712  leaddle0  11735  subge02  11736  halfaddsub  12483  avglt1  12488  hashssdif  14456  pythagtriplem4  16885  pythagtriplem14  16894  lsmss2  19743  grpoidinvlem2  30868  hvpncan3  31405  bcm1n  33151  revpfxsfxrev  35615  nnproddivdvdsd  42795  resubidaddlid  43184  reposdif  43257  3anidm12p1  45542  3impcombi  45553