Theorem an12s 655

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 651 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 651	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylbi 218	1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anabsan2  680  oecl  8462  oaass  8486  odi  8504  oen0  8512  oeworde  8519  ltexprlem4  10953  iccshftr  13430  iccshftl  13432  iccdil  13434  icccntr  13436  ndvdsadd  16370  eulerthlem2  16743  neips  23096  tx1stc  23633  filuni  23868  ufldom  23945  isch3  31330  unoplin  32009  hmoplin  32031  adjlnop  32175  chirredlem2  32480  btwnconn1lem12  36326  btwnconn1  36329  ttctr  36721  dfttc2g  36734  finxpreclem2  37752  poimirlem25  38012  mblfinlem4  38027  iscringd  38365  unichnidl  38398