Theorem ancom1s 666

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpt3fvot2d  7690  odi  8590  sornom  10358  leltadd  11803  divmul13  12023  absmax  15502  fzomaxdif  15516  dmatsgrp  22819  comppfsc  23856  iocopnst  25266  mumul  27513  lgsdir2  27662  branmfn  32712  chirredlem2  32998  chirredlem4  33000  icoreclin  38373  relowlssretop  38379  pibt2  38433  frinfm  38762  fzmul  38768  fdc  38772  rpnnen3  44132