Theorem anabsi5 666

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  anabsi6  667  anabsi8  669  3anidm12  1418  rspce  3550  onint  7640  f1oweALT  7815  php2OLD  9006  hasheqf1oi  14066  rtrclreclem3  14771  rtrclreclem4  14772  ablsimpgfindlem1  19710  ptcmpfi  22964  redwlk  28040  frgruhgr0v  28628  finxpreclem2  35561  finxpreclem6  35567  diophin  40594  diophun  40595  rspcegf  42566  stoweidlem36  43577