Theorem anabsi5 682

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 488	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2		anabsi5.1	. 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	mpcom 39	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anabsi6  683  anabsi8  685  3anidm12  1446  rspce  3565  onint  7790  f1oweALT  7970  hasheqf1oi  14416  rtrclreclem3  15134  rtrclreclem4  15135  ablsimpgfindlem1  20237  ptcmpfi  24040  redwlk  30131  frgruhgr0v  30745  finxpreclem2  38145  finxpreclem6  38151  diophin  43618  diophun  43619  rspcegf  45858  stoweidlem36  46865  grlimgrtri  48920