Theorem anabsi5 675

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

This theorem is referenced by:  anabsi6  676  anabsi8  678  3anidm12  1427  rspce  3549  onint  7733  f1oweALT  7914  hasheqf1oi  14304  rtrclreclem3  15013  rtrclreclem4  15014  ablsimpgfindlem1  20075  ptcmpfi  23796  redwlk  29757  frgruhgr0v  30352  finxpreclem2  37752  finxpreclem6  37758  diophin  43221  diophun  43222  rspcegf  45471  stoweidlem36  46479  grlimgrtri  48494