Theorem 3anidm12 1416

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

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

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3anidm13  1417  syl2an3an  1419  dedth3v  4486  nncan  10904  divid  11316  sqdivid  13484  subsq  13568  o1lo1  14886  retancl  15487  tanneg  15493  gcd0id  15857  coprm  16045  ablonncan  28339  kbpj  29739  xdivid  30630  xrsmulgzz  30712  f1resrcmplf1dlem  32469  expgrowthi  41037  dvconstbi  41038  3ornot23  41215  3anidm12p2  41513  sinhpcosh  45266  reseccl  45279  recsccl  45280  recotcl  45281  onetansqsecsq  45287