Theorem anabsi5 667

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  anabsi6  668  anabsi8  670  3anidm12  1415  rspce  3614  onint  7512  f1oweALT  7675  php2  8704  hasheqf1oi  13715  rtrclreclem3  14421  rtrclreclem4  14422  ablsimpgfindlem1  19231  ptcmpfi  22423  redwlk  27456  frgruhgr0v  28045  finxpreclem2  34673  finxpreclem6  34679  diophin  39376  diophun  39377  rspcegf  41287  stoweidlem36  42328