Theorem anabsi5 681

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anabsi6  682  anabsi8  684  3anidm12  1444  rspce  3579  onint  7788  f1oweALT  7968  hasheqf1oi  14386  rtrclreclem3  15096  rtrclreclem4  15097  ablsimpgfindlem1  20178  ptcmpfi  23938  redwlk  29960  frgruhgr0v  30555  finxpreclem2  37923  finxpreclem6  37929  diophin  43394  diophun  43395  rspcegf  45634  stoweidlem36  46641  grlimgrtri  48656