Theorem an12s 650

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 646 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 646	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylbi 217	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:  anabsan2  675  oecl  8474  oaass  8498  odi  8516  oen0  8524  oeworde  8531  ltexprlem4  10962  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  ndvdsadd  16349  eulerthlem2  16721  neips  23069  tx1stc  23606  filuni  23841  ufldom  23918  isch3  31329  unoplin  32008  hmoplin  32030  adjlnop  32174  chirredlem2  32479  btwnconn1lem12  36314  btwnconn1  36317  finxpreclem2  37645  poimirlem25  37896  mblfinlem4  37911  iscringd  38249  unichnidl  38282