Theorem anabsi5 668

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

This theorem is referenced by:  anabsi6  669  anabsi8  671  3anidm12  1416  rspce  3560  onint  7490  f1oweALT  7655  php2  8686  hasheqf1oi  13708  rtrclreclem3  14411  rtrclreclem4  14412  ablsimpgfindlem1  19222  ptcmpfi  22418  redwlk  27462  frgruhgr0v  28049  finxpreclem2  34807  finxpreclem6  34813  diophin  39713  diophun  39714  rspcegf  41652  stoweidlem36  42678