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  3566  onint  7804  f1oweALT  7984  hasheqf1oi  14495  rtrclreclem3  15213  rtrclreclem4  15214  ablsimpgfindlem1  20323  ptcmpfi  24132  redwlk  30251  frgruhgr0v  30865  finxpreclem2  38313  finxpreclem6  38319  diophin  43782  diophun  43783  rspcegf  46039  stoweidlem36  47045  grlimgrtri  49100