Theorem anabsi5 659

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		anabsi5.1	. . 3 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))
2	1	imp 397	. 2 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒)
3	2	anabss5 658	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  anabsi6  660  anabsi8  662  3anidm12  1491  rspce  3506  onint  7275  f1oweALT  7431  php2  8435  hasheqf1oi  13463  rtrclreclem3  14213  rtrclreclem4  14214  ptcmpfi  22036  redwlk  27040  frgruhgr0v  27688  finxpreclem2  33829  finxpreclem6  33835  diophin  38310  diophun  38311  rspcegf  40129  stoweidlem36  41194