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  3577  onint  7766  f1oweALT  7951  hasheqf1oi  14316  rtrclreclem3  15026  rtrclreclem4  15027  ablsimpgfindlem1  20039  ptcmpfi  23700  redwlk  29600  frgruhgr0v  30193  finxpreclem2  37378  finxpreclem6  37384  diophin  42760  diophun  42761  rspcegf  45017  stoweidlem36  46034  grlimgrtri  47995