Theorem 3anidm13 1418

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

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

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 1087

This theorem is referenced by:  npncan2  11178  ltsubpos  11397  leaddle0  11420  subge02  11421  halfaddsub  12136  avglt1  12141  hashssdif  14055  pythagtriplem4  16448  pythagtriplem14  16457  lsmss2  19188  grpoidinvlem2  28768  hvpncan3  29305  bcm1n  31018  revpfxsfxrev  32977  nnproddivdvdsd  39937  resubidaddid1  40299  reposdif  40345  3anidm12p1  42315  3impcombi  42326