Theorem 3anidm12 1444

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3anidm13  1445  syl2an3an  1447  dedth3v  4554  fovcl  7539  nncan  11487  divid  11902  sqdivid  14158  subsq  14246  o1lo1  15588  retancl  16198  tanneg  16204  gcd0id  16577  coprm  16770  ablonncan  30849  kbpj  32249  xdivid  33188  xrsmulgzz  33270  f1resrcmplf1dlem  35418  expgrowthi  44970  dvconstbi  44971  3ornot23  45145  3anidm12p2  45442  sinhpcosh  50438  reseccl  50451  recsccl  50452  recotcl  50453  onetansqsecsq  50459