Theorem anabsi5 665

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  anabsi6  666  anabsi8  668  3anidm12  1417  rspce  3600  onint  7780  f1oweALT  7961  php2OLD  9225  hasheqf1oi  14315  rtrclreclem3  15011  rtrclreclem4  15012  ablsimpgfindlem1  20018  ptcmpfi  23537  redwlk  29196  frgruhgr0v  29784  finxpreclem2  36574  finxpreclem6  36580  diophin  41812  diophun  41813  rspcegf  44009  stoweidlem36  45050