Theorem anabsi5 669

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anabsi6  670  anabsi8  672  3anidm12  1421  rspce  3565  onint  7735  f1oweALT  7916  hasheqf1oi  14274  rtrclreclem3  14983  rtrclreclem4  14984  ablsimpgfindlem1  20038  ptcmpfi  23757  redwlk  29744  frgruhgr0v  30339  finxpreclem2  37595  finxpreclem6  37601  diophin  43014  diophun  43015  rspcegf  45268  stoweidlem36  46280  grlimgrtri  48249