Theorem 3anidm12 1421

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anidm13  1422  syl2an3an  1424  dedth3v  4540  fovcl  7477  nncan  11393  divid  11810  dividOLD  11811  sqdivid  14029  subsq  14117  o1lo1  15444  retancl  16051  tanneg  16057  gcd0id  16430  coprm  16622  ablonncan  30500  kbpj  31900  xdivid  32869  xrsmulgzz  32964  f1resrcmplf1dlem  35059  expgrowthi  44316  dvconstbi  44317  3ornot23  44493  3anidm12p2  44790  sinhpcosh  49735  reseccl  49748  recsccl  49749  recotcl  49750  onetansqsecsq  49756