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 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:  3anidm13  1418  syl2an3an  1420  dedth3v  4590  fovcl  7539  nncan  11493  divid  11905  sqdivid  14091  subsq  14178  o1lo1  15485  retancl  16089  tanneg  16095  gcd0id  16464  coprm  16652  ablonncan  30076  kbpj  31476  xdivid  32361  xrsmulgzz  32446  f1resrcmplf1dlem  34387  expgrowthi  43394  dvconstbi  43395  3ornot23  43572  3anidm12p2  43870  sinhpcosh  47872  reseccl  47885  recsccl  47886  recotcl  47887  onetansqsecsq  47893