Theorem anabsi5 665

Description: Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)

Hypothesis

Ref	Expression
anabsi5.1	⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))

Assertion

Ref	Expression
anabsi5	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem anabsi5

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2		anabsi5.1	. 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	mpcom 38	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  anabsi6  666  anabsi8  668  3anidm12  1417  rspce  3540  onint  7617  f1oweALT  7788  php2  8898  hasheqf1oi  13994  rtrclreclem3  14699  rtrclreclem4  14700  ablsimpgfindlem1  19625  ptcmpfi  22872  redwlk  27942  frgruhgr0v  28529  finxpreclem2  35488  finxpreclem6  35494  diophin  40510  diophun  40511  rspcegf  42455  stoweidlem36  43467