Theorem 3anidm12 1415

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3anidm13  1416  syl2an3an  1418  dedth3v  4530  nncan  10917  divid  11329  sqdivid  13491  subsq  13575  o1lo1  14896  retancl  15497  tanneg  15503  gcd0id  15869  coprm  16057  ablonncan  28335  kbpj  29735  xdivid  30606  xrsmulgzz  30667  f1resrcmplf1dlem  32361  expgrowthi  40672  dvconstbi  40673  3ornot23  40850  3anidm12p2  41148  sinhpcosh  44846  reseccl  44859  recsccl  44860  recotcl  44861  onetansqsecsq  44867