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  1446  rspce  3570  onint  7785  f1oweALT  7965  hasheqf1oi  14383  rtrclreclem3  15093  rtrclreclem4  15094  ablsimpgfindlem1  20174  ptcmpfi  23970  redwlk  30020  frgruhgr0v  30615  finxpreclem2  38036  finxpreclem6  38042  diophin  43503  diophun  43504  rspcegf  45743  stoweidlem36  46750  grlimgrtri  48768