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  1447  rspce  3569  onint  7838  f1oweALT  8018  hasheqf1oi  14536  rtrclreclem3  15256  rtrclreclem4  15257  ablsimpgfindlem1  20374  ptcmpfi  24187  redwlk  30308  frgruhgr0v  30922  finxpreclem2  38581  finxpreclem6  38587  diophin  44049  diophun  44050  rspcegf  46314  stoweidlem36  47319  grlimgrtri  49374