Theorem anabsi5 853

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 443	. 2 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒)
3	2	anabss5 852	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  anabsi6  854  anabsi8  856  3anidm12  1374  rspce  3276  onint  6864  f1oweALT  7020  php2  8007  hasheqf1oi  12954  hasheqf1oiOLD  12955  rtrclreclem3  13594  rtrclreclem4  13595  ptcmpfi  21368  redwlk  25902  vdusgraval  26200  finxpreclem2  32206  finxpreclem6  32212  diophin  36157  diophun  36158  rspcegf  38008  rspcef  38070  stoweidlem36  38733  red1wlk  40883  frgruhgr0v  41437