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 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  669  anabsi8  671  3anidm12  1419  rspce  3624  onint  7826  f1oweALT  8013  php2OLD  9286  hasheqf1oi  14400  rtrclreclem3  15109  rtrclreclem4  15110  ablsimpgfindlem1  20151  ptcmpfi  23842  redwlk  29708  frgruhgr0v  30296  finxpreclem2  37356  finxpreclem6  37362  diophin  42728  diophun  42729  rspcegf  44923  stoweidlem36  45957  grlimgrtri  47820