Theorem 3anidm12 1332

Description: Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)

Hypothesis

Ref	Expression
3anidm12.1	⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3anidm12	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem 3anidm12

Step	Hyp	Ref	Expression
1		3anidm12.1	. . 3 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)
2	1	3expib 1233	. 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))
3	2	anabsi5 581	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3anidm13  1333  syl2an3an  1335  fovcl  6167  prarloclemarch2  7750  nq02m  7796  recexprlem1ssl  7964  recexprlem1ssu  7965  nncan  8518  dividap  8992  modqid0  10736  sqdividap  10990  subsq  11032  retanclap  12433  tannegap  12439  gcd0id  12700  coprm  12866