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  3612  onint  7510  f1oweALT  7673  php2  8702  hasheqf1oi  13713  rtrclreclem3  14419  rtrclreclem4  14420  ablsimpgfindlem1  19229  ptcmpfi  22421  redwlk  27454  frgruhgr0v  28043  finxpreclem2  34674  finxpreclem6  34680  diophin  39389  diophun  39390  rspcegf  41300  stoweidlem36  42341