Theorem ancom1s 663

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 463	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 589	1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  odi  8543  sornom  10231  leltadd  11668  divmul13  11891  absmax  15340  fzomaxdif  15354  dmatsgrp  22539  comppfsc  23572  iocopnst  24982  mumul  27222  lgsdir2  27371  branmfn  32254  chirredlem2  32540  chirredlem4  32542  icoreclin  37815  relowlssretop  37821  pibt2  37875  frinfm  38198  fzmul  38204  fdc  38208  rpnnen3  43573