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  4545  fovcl  7498  nncan  11424  divid  11841  dividOLD  11842  sqdivid  14059  subsq  14147  o1lo1  15474  retancl  16081  tanneg  16087  gcd0id  16460  coprm  16652  ablonncan  30650  kbpj  32050  xdivid  33026  xrsmulgzz  33108  f1resrcmplf1dlem  35269  expgrowthi  44718  dvconstbi  44719  3ornot23  44894  3anidm12p2  45191  sinhpcosh  50128  reseccl  50141  recsccl  50142  recotcl  50143  onetansqsecsq  50149