Theorem anabsi5 669

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

This theorem is referenced by:  anabsi6  670  anabsi8  672  3anidm12  1421  rspce  3561  onint  7723  f1oweALT  7904  hasheqf1oi  14258  rtrclreclem3  14967  rtrclreclem4  14968  ablsimpgfindlem1  20021  ptcmpfi  23728  redwlk  29649  frgruhgr0v  30244  finxpreclem2  37434  finxpreclem6  37440  diophin  42875  diophun  42876  rspcegf  45130  stoweidlem36  46144  grlimgrtri  48113