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  11512  ltsubpos  11733  leaddle0  11756  subge02  11757  halfaddsub  12504  avglt1  12509  hashssdif  14479  revpfxsfxrev  14839  pythagtriplem4  16915  pythagtriplem14  16924  lsmss2  19795  grpoidinvlem2  30972  hvpncan3  31509  bcm1n  33253  nnproddivdvdsd  42853  resubidaddlid  43257  reposdif  43330  3anidm12p1  45615  3impcombi  45626