Theorem 3anidm12 1420

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 1123	. 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))
3	2	anabsi5 669	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  3anidm13  1421  syl2an3an  1423  dedth3v  4478  nncan  10996  divid  11408  sqdivid  13583  subsq  13667  o1lo1  14987  retancl  15590  tanneg  15596  gcd0id  15965  coprm  16155  ablonncan  28494  kbpj  29894  xdivid  30780  xrsmulgzz  30867  f1resrcmplf1dlem  32632  expgrowthi  41512  dvconstbi  41513  3ornot23  41690  3anidm12p2  41988  sinhpcosh  45925  reseccl  45938  recsccl  45939  recotcl  45940  onetansqsecsq  45946