Theorem 3anidm12 1418

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anidm13  1419  syl2an3an  1421  dedth3v  4523  nncan  11259  divid  11671  sqdivid  13851  subsq  13935  o1lo1  15255  retancl  15860  tanneg  15866  gcd0id  16235  coprm  16425  ablonncan  28927  kbpj  30327  xdivid  31211  xrsmulgzz  31296  f1resrcmplf1dlem  33067  expgrowthi  41958  dvconstbi  41959  3ornot23  42136  3anidm12p2  42434  sinhpcosh  46453  reseccl  46466  recsccl  46467  recotcl  46468  onetansqsecsq  46474