Theorem anabsi5 682

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anabsi6  683  anabsi8  685  3anidm12  1446  rspce  3572  onint  7795  f1oweALT  7975  hasheqf1oi  14407  rtrclreclem3  15123  rtrclreclem4  15124  ablsimpgfindlem1  20225  ptcmpfi  24023  redwlk  30080  frgruhgr0v  30688  finxpreclem2  38095  finxpreclem6  38101  diophin  43563  diophun  43564  rspcegf  45803  stoweidlem36  46810  grlimgrtri  48828