Theorem anabsi5 858

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  anabsi6  859  anabsi8  861  3anidm12  1383  rspce  3304  onint  6995  f1oweALT  7152  php2  8145  hasheqf1oi  13140  hasheqf1oiOLD  13141  rtrclreclem3  13800  rtrclreclem4  13801  ptcmpfi  21616  redwlk  26569  frgruhgr0v  27127  finxpreclem2  33227  finxpreclem6  33233  diophin  37336  diophun  37337  rspcegf  39182  stoweidlem36  40253