Theorem 3anidm12 1440

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

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

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  3anidm13  1441  syl2an3an  1443  dedth3v  4546  fovcl  7526  nncan  11462  divid  11878  dividOLD  11879  sqdivid  14137  subsq  14225  o1lo1  15566  retancl  16176  tanneg  16182  gcd0id  16555  coprm  16748  ablonncan  30761  kbpj  32161  xdivid  33107  xrsmulgzz  33189  f1resrcmplf1dlem  35382  expgrowthi  44914  dvconstbi  44915  3ornot23  45090  3anidm12p2  45387  sinhpcosh  50366  reseccl  50379  recsccl  50380  recotcl  50381  onetansqsecsq  50387