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 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  npncan2  11491  ltsubpos  11710  leaddle0  11733  subge02  11734  halfaddsub  12449  avglt1  12454  hashssdif  14376  pythagtriplem4  16756  pythagtriplem14  16765  lsmss2  19576  grpoidinvlem2  30025  hvpncan3  30562  bcm1n  32273  revpfxsfxrev  34404  nnproddivdvdsd  41172  resubidaddlid  41570  reposdif  41618  3anidm12p1  43869  3impcombi  43880