Theorem 3anidm12 1447

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  1448  syl2an3an  1450  dedth3v  4549  f1resrcmplf1dlem  7298  fovcl  7568  tz7.48lem  8475  nncan  11611  divid  12028  sqdivid  14289  subsq  14378  o1lo1  15730  retancl  16336  tanneg  16342  gcd0id  16717  coprm  16913  ablonncan  31185  kbpj  32585  xdivid  33561  xrsmulgzz  33637  expgrowthi  45507  dvconstbi  45508  3ornot23  45681  3anidm12p2  45978  sinhpcosh  51111  reseccl  51124  recsccl  51125  recotcl  51126  onetansqsecsq  51132