Theorem an12s 649

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 645 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 645	. 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  674  oecl  8464  oaass  8488  odi  8506  oen0  8514  oeworde  8521  ltexprlem4  10950  iccshftr  13402  iccshftl  13404  iccdil  13406  icccntr  13408  ndvdsadd  16337  eulerthlem2  16709  neips  23057  tx1stc  23594  filuni  23829  ufldom  23906  isch3  31316  unoplin  31995  hmoplin  32017  adjlnop  32161  chirredlem2  32466  btwnconn1lem12  36292  btwnconn1  36295  finxpreclem2  37595  poimirlem25  37846  mblfinlem4  37861  iscringd  38199  unichnidl  38232