Theorem 3anidm12 1428

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  3anidm13  1429  syl2an3an  1431  dedth3v  4521  fovcl  7488  nncan  11418  divid  11835  dividOLD  11836  sqdivid  14079  subsq  14167  o1lo1  15494  retancl  16104  tanneg  16110  gcd0id  16483  coprm  16676  ablonncan  30649  kbpj  32049  xdivid  33010  xrsmulgzz  33092  f1resrcmplf1dlem  35282  expgrowthi  44792  dvconstbi  44793  3ornot23  44968  3anidm12p2  45265  sinhpcosh  50244  reseccl  50257  recsccl  50258  recotcl  50259  onetansqsecsq  50265