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  4546  f1resrcmplf1dlem  7272  fovcl  7542  tz7.48lem  8432  nncan  11514  divid  11929  sqdivid  14189  subsq  14277  o1lo1  15627  retancl  16233  tanneg  16239  gcd0id  16612  coprm  16805  ablonncan  31040  kbpj  32440  xdivid  33376  xrsmulgzz  33452  expgrowthi  45160  dvconstbi  45161  3ornot23  45335  3anidm12p2  45632  sinhpcosh  50669  reseccl  50682  recsccl  50683  recotcl  50684  onetansqsecsq  50690