Theorem ancom1s 654

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 581	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  8514  sornom  10199  leltadd  11634  divmul13  11858  absmax  15292  fzomaxdif  15306  dmatsgrp  22464  comppfsc  23497  iocopnst  24907  mumul  27144  lgsdir2  27293  branmfn  32176  chirredlem2  32462  chirredlem4  32464  icoreclin  37673  relowlssretop  37679  pibt2  37733  frinfm  38056  fzmul  38062  fdc  38066  rpnnen3  43460