Theorem anabsi5 670

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  671  anabsi8  673  3anidm12  1422  rspce  3554  onint  7738  f1oweALT  7919  hasheqf1oi  14307  rtrclreclem3  15016  rtrclreclem4  15017  ablsimpgfindlem1  20078  ptcmpfi  23791  redwlk  29757  frgruhgr0v  30352  finxpreclem2  37723  finxpreclem6  37729  diophin  43221  diophun  43222  rspcegf  45475  stoweidlem36  46485  grlimgrtri  48494