Theorem 3anidm12 1422

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anidm13  1423  syl2an3an  1425  dedth3v  4544  fovcl  7488  nncan  11414  divid  11831  dividOLD  11832  sqdivid  14049  subsq  14137  o1lo1  15464  retancl  16071  tanneg  16077  gcd0id  16450  coprm  16642  ablonncan  30635  kbpj  32035  xdivid  33011  xrsmulgzz  33093  f1resrcmplf1dlem  35244  expgrowthi  44641  dvconstbi  44642  3ornot23  44817  3anidm12p2  45114  sinhpcosh  50052  reseccl  50065  recsccl  50066  recotcl  50067  onetansqsecsq  50073