Theorem 3anidm12 1421

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anidm13  1422  syl2an3an  1424  dedth3v  4552  fovcl  7517  nncan  11451  divid  11868  dividOLD  11869  sqdivid  14087  subsq  14175  o1lo1  15503  retancl  16110  tanneg  16116  gcd0id  16489  coprm  16681  ablonncan  30485  kbpj  31885  xdivid  32848  xrsmulgzz  32947  f1resrcmplf1dlem  35076  expgrowthi  44322  dvconstbi  44323  3ornot23  44499  3anidm12p2  44796  sinhpcosh  49726  reseccl  49739  recsccl  49740  recotcl  49741  onetansqsecsq  49747