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  4530  fovcl  7495  nncan  11423  divid  11840  dividOLD  11841  sqdivid  14084  subsq  14172  o1lo1  15499  retancl  16109  tanneg  16115  gcd0id  16488  coprm  16681  ablonncan  30627  kbpj  32027  xdivid  32987  xrsmulgzz  33069  f1resrcmplf1dlem  35229  expgrowthi  44760  dvconstbi  44761  3ornot23  44936  3anidm12p2  45233  sinhpcosh  50215  reseccl  50228  recsccl  50229  recotcl  50230  onetansqsecsq  50236