Theorem anabsi7 669

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 668	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3	2	ancoms 461	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  nelrdva  3699  elunii  4846  ordelord  6216  fvelrn  6847  onsucuni2  7552  fnfi  8799  prnmax  10420  relexpindlem  14425  opreu2reuALT  30243  ralssiun  34692  monotoddzz  39546  oddcomabszz  39547  flcidc  39780  syldbl2  40525  fmul01  41867  fprodcnlem  41886  stoweidlem4  42296  stoweidlem20  42312  stoweidlem22  42314  stoweidlem27  42319  stoweidlem30  42322  stoweidlem51  42343  stoweidlem59  42351  fourierdlem21  42420  fourierdlem89  42487  fourierdlem90  42488  fourierdlem91  42489  fourierdlem104  42502