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  4548  fovcl  7497  nncan  11427  divid  11844  dividOLD  11845  sqdivid  14063  subsq  14151  o1lo1  15479  retancl  16086  tanneg  16092  gcd0id  16465  coprm  16657  ablonncan  30535  kbpj  31935  xdivid  32898  xrsmulgzz  32993  f1resrcmplf1dlem  35069  expgrowthi  44315  dvconstbi  44316  3ornot23  44492  3anidm12p2  44789  sinhpcosh  49722  reseccl  49735  recsccl  49736  recotcl  49737  onetansqsecsq  49743