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  4536  fovcl  7474  nncan  11390  divid  11807  dividOLD  11808  sqdivid  14029  subsq  14117  o1lo1  15444  retancl  16051  tanneg  16057  gcd0id  16430  coprm  16622  ablonncan  30536  kbpj  31936  xdivid  32908  xrsmulgzz  32990  f1resrcmplf1dlem  35098  expgrowthi  44425  dvconstbi  44426  3ornot23  44601  3anidm12p2  44898  sinhpcosh  49840  reseccl  49853  recsccl  49854  recotcl  49855  onetansqsecsq  49861