Theorem ancom1s 665

Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

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

Assertion

Ref	Expression
ancom1s	⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃)

Proof of Theorem ancom1s

Step	Hyp	Ref	Expression
1		pm3.22 464	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 591	1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  odi  8565  sornom  10262  leltadd  11699  divmul13  11919  absmax  15383  fzomaxdif  15397  dmatsgrp  22637  comppfsc  23670  iocopnst  25080  mumul  27323  lgsdir2  27472  branmfn  32435  chirredlem2  32721  chirredlem4  32723  icoreclin  37981  relowlssretop  37987  pibt2  38041  frinfm  38364  fzmul  38370  fdc  38374  rpnnen3  43739