Theorem 3anidm12 1419

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 668	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

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

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 1089

This theorem is referenced by:  3anidm13  1420  syl2an3an  1422  dedth3v  4611  fovcl  7578  nncan  11565  divid  11980  dividOLD  11981  sqdivid  14172  subsq  14259  o1lo1  15583  retancl  16190  tanneg  16196  gcd0id  16565  coprm  16758  ablonncan  30588  kbpj  31988  xdivid  32892  xrsmulgzz  32992  f1resrcmplf1dlem  35062  expgrowthi  44302  dvconstbi  44303  3ornot23  44480  3anidm12p2  44778  sinhpcosh  48832  reseccl  48845  recsccl  48846  recotcl  48847  onetansqsecsq  48853