Theorem 3anidm12 1446

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anidm13  1447  syl2an3an  1449  dedth3v  4545  f1resrcmplf1dlem  7278  fovcl  7548  tz7.48lem  8450  nncan  11587  divid  12004  sqdivid  14265  subsq  14354  o1lo1  15704  retancl  16310  tanneg  16316  gcd0id  16691  coprm  16887  ablonncan  31158  kbpj  32558  xdivid  33494  xrsmulgzz  33570  expgrowthi  45317  dvconstbi  45318  3ornot23  45492  3anidm12p2  45789  sinhpcosh  50833  reseccl  50846  recsccl  50847  recotcl  50848  onetansqsecsq  50854