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  4527  nncan  10914  divid  11326  sqdivid  13487  subsq  13571  o1lo1  14893  retancl  15494  tanneg  15500  gcd0id  15866  coprm  16054  ablonncan  28332  kbpj  29732  xdivid  30604  xrsmulgzz  30665  f1resrcmplf1dlem  32359  expgrowthi  40663  dvconstbi  40664  3ornot23  40841  3anidm12p2  41139  sinhpcosh  44838  reseccl  44851  recsccl  44852  recotcl  44853  onetansqsecsq  44859