Theorem an12s 839

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 834 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.)

Hypothesis

Ref	Expression
an12s.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
an12s	⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃)

Proof of Theorem an12s

Step	Hyp	Ref	Expression
1		an12 834	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylbi 206	1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anabsan2  859  1stconst  7152  2ndconst  7153  oecl  7504  oaass  7528  odi  7546  oen0  7553  oeworde  7560  ltexprlem4  9740  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  ndvdsadd  14972  eulerthlem2  15325  neips  20727  tx1stc  21263  filuni  21499  ufldom  21576  isch3  27482  unoplin  28163  hmoplin  28185  adjlnop  28329  chirredlem2  28634  btwnconn1lem12  31375  btwnconn1  31378  finxpreclem2  32403  poimirlem25  32604  mblfinlem4  32619  iscringd  32967  unichnidl  33000