Theorem 3anidm13 1448

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 1447	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  11609  ltsubpos  11832  leaddle0  11855  subge02  11856  halfaddsub  12603  avglt1  12608  hashssdif  14581  revpfxsfxrev  14942  pythagtriplem4  17023  pythagtriplem14  17032  lsmss2  19908  grpoidinvlem2  31134  hvpncan3  31671  bcm1n  33454  nnproddivdvdsd  43241  resubidaddlid  43637  reposdif  43710  3anidm12p1  45977  3impcombi  45988