Theorem anabsi7 668

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 667	. 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 206  df-an 397

This theorem is referenced by:  syldbl2  838  nelrdva  3640  elunii  4844  ordelord  6288  fvelrn  6954  onsucuni2  7681  fnfi  8964  prnmax  10751  relexpindlem  14774  opreu2reuALT  30825  ralssiun  35578  monotoddzz  40765  oddcomabszz  40766  flcidc  40999  fmul01  43121  fprodcnlem  43140  stoweidlem4  43545  stoweidlem20  43561  stoweidlem22  43563  stoweidlem27  43568  stoweidlem30  43571  stoweidlem51  43592  stoweidlem59  43600  fourierdlem21  43669  fourierdlem89  43736  fourierdlem90  43737  fourierdlem91  43738  fourierdlem104  43751