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  8466  oaass  8490  odi  8508  oen0  8516  oeworde  8523  ltexprlem4  10956  iccshftr  13433  iccshftl  13435  iccdil  13437  icccntr  13439  ndvdsadd  16373  eulerthlem2  16746  neips  23091  tx1stc  23628  filuni  23863  ufldom  23940  isch3  31330  unoplin  32009  hmoplin  32031  adjlnop  32175  chirredlem2  32480  btwnconn1lem12  36299  btwnconn1  36302  ttctr  36694  dfttc2g  36707  finxpreclem2  37723  poimirlem25  37983  mblfinlem4  37998  iscringd  38336  unichnidl  38369