Theorem 3anidm12 1445

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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

This theorem is used by:  3anidm13  1446  syl2an3an  1448  dedth3v  4550  fovcl  7540  nncan  11493  divid  11908  sqdivid  14165  subsq  14253  o1lo1  15595  retancl  16204  tanneg  16210  gcd0id  16583  coprm  16776  ablonncan  30919  kbpj  32319  xdivid  33258  xrsmulgzz  33338  f1resrcmplf1dlem  35483  expgrowthi  45071  dvconstbi  45072  3ornot23  45246  3anidm12p2  45543  sinhpcosh  50546  reseccl  50559  recsccl  50560  recotcl  50561  onetansqsecsq  50567