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  3553  onint  7744  f1oweALT  7925  hasheqf1oi  14313  rtrclreclem3  15022  rtrclreclem4  15023  ablsimpgfindlem1  20084  ptcmpfi  23778  redwlk  29739  frgruhgr0v  30334  finxpreclem2  37706  finxpreclem6  37712  diophin  43204  diophun  43205  rspcegf  45454  stoweidlem36  46464  grlimgrtri  48479