Theorem anabsi5 893

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

Syntax hints:   → wi 4   ∧ wa 383

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 385

This theorem is referenced by:  anabsi6  894  anabsi8  896  3anidm12  1530  rspce  3444  onint  7160  f1oweALT  7317  php2  8310  hasheqf1oi  13334  rtrclreclem3  13999  rtrclreclem4  14000  ptcmpfi  21818  redwlk  26779  frgruhgr0v  27417  finxpreclem2  33538  finxpreclem6  33544  diophin  37838  diophun  37839  rspcegf  39681  stoweidlem36  40756