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:  odi  8571  sornom  10336  leltadd  11781  divmul13  12001  absmax  15477  fzomaxdif  15491  dmatsgrp  22794  comppfsc  23831  iocopnst  25241  mumul  27490  lgsdir2  27639  branmfn  32689  chirredlem2  32975  chirredlem4  32977  icoreclin  38248  relowlssretop  38254  pibt2  38308  frinfm  38637  fzmul  38643  fdc  38647  rpnnen3  43992