Theorem 3anidm12 1417

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 1120	. 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))
3	2	anabsi5 665	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:  3anidm13  1418  syl2an3an  1420  dedth3v  4519  nncan  11180  divid  11592  sqdivid  13770  subsq  13854  o1lo1  15174  retancl  15779  tanneg  15785  gcd0id  16154  coprm  16344  ablonncan  28819  kbpj  30219  xdivid  31104  xrsmulgzz  31189  f1resrcmplf1dlem  32958  expgrowthi  41840  dvconstbi  41841  3ornot23  42018  3anidm12p2  42316  sinhpcosh  46328  reseccl  46341  recsccl  46342  recotcl  46343  onetansqsecsq  46349