Theorem anabsi7 667

Description: Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)

Hypothesis

Ref	Expression
anabsi7.1	⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒))

Assertion

Ref	Expression
anabsi7	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem anabsi7

Step	Hyp	Ref	Expression
1		anabsi7.1	. . 3 ⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒))
2	1	anabsi6 666	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3	2	ancoms 458	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  syldbl2  837  nelrdva  3635  elunii  4841  ordelord  6273  fvelrn  6936  onsucuni2  7656  fnfi  8925  prnmax  10682  relexpindlem  14702  opreu2reuALT  30726  ralssiun  35505  monotoddzz  40681  oddcomabszz  40682  flcidc  40915  fmul01  43011  fprodcnlem  43030  stoweidlem4  43435  stoweidlem20  43451  stoweidlem22  43453  stoweidlem27  43458  stoweidlem30  43461  stoweidlem51  43482  stoweidlem59  43490  fourierdlem21  43559  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem104  43641