Theorem anabsi5 679

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anabsi6  680  anabsi8  682  3anidm12  1438  rspce  3570  onint  7773  f1oweALT  7953  hasheqf1oi  14364  rtrclreclem3  15073  rtrclreclem4  15074  ablsimpgfindlem1  20149  ptcmpfi  23873  redwlk  29871  frgruhgr0v  30466  finxpreclem2  37884  finxpreclem6  37890  diophin  43353  diophun  43354  rspcegf  45603  stoweidlem36  46610  grlimgrtri  48625