Theorem 3anidm12 1543

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

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  3anidm13  1544  syl2an3an  1546  dedth3v  4338  nncan  10602  divid  11006  sqdivid  13183  subsq  13226  o1lo1  14609  retancl  15208  tanneg  15214  gcd0id  15575  coprm  15756  ablonncan  27936  kbpj  29340  xdivid  30152  xrsmulgzz  30194  expgrowthi  39314  dvconstbi  39315  3ornot23  39495  3anidm12p2  39803  sinhpcosh  43283  reseccl  43296  recsccl  43297  recotcl  43298  onetansqsecsq  43304