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  4549  f1resrcmplf1dlem  7274  fovcl  7544  nncan  11514  divid  11929  sqdivid  14188  subsq  14276  o1lo1  15626  retancl  16234  tanneg  16240  gcd0id  16613  coprm  16806  ablonncan  31023  kbpj  32423  xdivid  33360  xrsmulgzz  33436  expgrowthi  45144  dvconstbi  45145  3ornot23  45319  3anidm12p2  45616  sinhpcosh  50653  reseccl  50666  recsccl  50667  recotcl  50668  onetansqsecsq  50674