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  7267  fovcl  7537  tz7.48lem  8429  nncan  11544  divid  11959  sqdivid  14219  subsq  14307  o1lo1  15657  retancl  16263  tanneg  16269  gcd0id  16642  coprm  16835  ablonncan  31077  kbpj  32477  xdivid  33413  xrsmulgzz  33489  expgrowthi  45255  dvconstbi  45256  3ornot23  45430  3anidm12p2  45727  sinhpcosh  50749  reseccl  50762  recsccl  50763  recotcl  50764  onetansqsecsq  50770