Theorem anabsi5 669

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  670  anabsi8  672  3anidm12  1421  rspce  3580  onint  7769  f1oweALT  7954  hasheqf1oi  14323  rtrclreclem3  15033  rtrclreclem4  15034  ablsimpgfindlem1  20046  ptcmpfi  23707  redwlk  29607  frgruhgr0v  30200  finxpreclem2  37385  finxpreclem6  37391  diophin  42767  diophun  42768  rspcegf  45024  stoweidlem36  46041  grlimgrtri  47999