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 459	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  nelrdva  3637  elunii  4756  ordelord  6095  fvelrn  6716  onsucuni2  7412  fnfi  8649  prnmax  10270  relexpindlem  14260  opreu2reuALT  29928  ralssiun  34240  monotoddzz  39046  oddcomabszz  39047  flcidc  39280  syldbl2  40025  fmul01  41424  fprodcnlem  41443  stoweidlem4  41853  stoweidlem20  41869  stoweidlem22  41871  stoweidlem27  41876  stoweidlem30  41879  stoweidlem51  41900  stoweidlem59  41908  fourierdlem21  41977  fourierdlem89  42044  fourierdlem90  42045  fourierdlem91  42046  fourierdlem104  42059