Theorem 3anidm13 1419

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  npncan2  11534  ltsubpos  11753  leaddle0  11776  subge02  11777  halfaddsub  12497  avglt1  12502  hashssdif  14448  pythagtriplem4  16853  pythagtriplem14  16862  lsmss2  19700  grpoidinvlem2  30534  hvpncan3  31071  bcm1n  32803  revpfxsfxrev  35100  nnproddivdvdsd  41982  resubidaddlid  42402  reposdif  42450  3anidm12p1  44804  3impcombi  44815