Theorem 3anidm12 1375

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3anidm13  1376  syl2an3an  1378  dedth3v  4094  nncan  10189  divid  10593  sqdivid  12791  subsq  12834  o1lo1  14116  retancl  14711  tanneg  14717  gcd0id  15078  coprm  15261  ablonncan  26795  kbpj  28199  xdivid  28967  xrsmulgzz  29009  expgrowthi  37554  dvconstbi  37555  3ornot23  37736  3anidm12p2  38055  sinhpcosh  42280  reseccl  42293  recsccl  42294  recotcl  42295  onetansqsecsq  42301