Theorem anabsi5 670

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  671  anabsi8  673  3anidm12  1422  rspce  3567  onint  7745  f1oweALT  7926  hasheqf1oi  14286  rtrclreclem3  14995  rtrclreclem4  14996  ablsimpgfindlem1  20050  ptcmpfi  23769  redwlk  29756  frgruhgr0v  30351  finxpreclem2  37645  finxpreclem6  37651  diophin  43129  diophun  43130  rspcegf  45383  stoweidlem36  46394  grlimgrtri  48363