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 206  df-an 396  df-3an 1088

This theorem is referenced by:  npncan2  11492  ltsubpos  11711  leaddle0  11734  subge02  11735  halfaddsub  12450  avglt1  12455  hashssdif  14377  pythagtriplem4  16757  pythagtriplem14  16766  lsmss2  19577  grpoidinvlem2  30026  hvpncan3  30563  bcm1n  32274  revpfxsfxrev  34405  nnproddivdvdsd  41173  resubidaddlid  41571  reposdif  41619  3anidm12p1  43870  3impcombi  43881