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  7808  f1oweALT  7988  hasheqf1oi  14502  rtrclreclem3  15222  rtrclreclem4  15223  ablsimpgfindlem1  20332  ptcmpfi  24141  redwlk  30260  frgruhgr0v  30874  finxpreclem2  38450  finxpreclem6  38456  diophin  43920  diophun  43921  rspcegf  46176  stoweidlem36  47182  grlimgrtri  49237