Theorem ancom1s 653

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  odi  8618  sornom  10318  leltadd  11748  divmul13  11971  absmax  15369  fzomaxdif  15383  dmatsgrp  22506  comppfsc  23541  iocopnst  24971  mumul  27225  lgsdir2  27375  branmfn  32125  chirredlem2  32411  chirredlem4  32413  icoreclin  37359  relowlssretop  37365  pibt2  37419  frinfm  37743  fzmul  37749  fdc  37753  rpnnen3  43049