Theorem anabsi7 856

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 855	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3	2	ancoms 468	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 196  df-an 385

This theorem is referenced by:  syl2an23an  1379  nelrdva  3384  elunii  4377  ordelord  5662  fvelrn  6260  onsucuni2  6926  fnfi  8123  prnmax  9696  monotoddzz  36526  oddcomabszz  36527  flcidc  36763  syldbl2  37490  fmul01  38647  fprodcnlem  38666  stoweidlem4  38897  stoweidlem20  38913  stoweidlem22  38915  stoweidlem27  38920  stoweidlem30  38923  stoweidlem51  38944  stoweidlem59  38952  fourierdlem21  39021  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem104  39103