Theorem an12s 659

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anabsan2  684  oecl  8506  oaass  8530  odi  8548  oen0  8556  oeworde  8563  ltexprlem4  10997  iccshftr  13490  iccshftl  13492  iccdil  13494  icccntr  13496  ndvdsadd  16444  eulerthlem2  16817  neips  23173  tx1stc  23710  filuni  23945  ufldom  24022  isch3  31444  unoplin  32123  hmoplin  32145  adjlnop  32289  chirredlem2  32594  btwnconn1lem12  36448  btwnconn1  36451  ttctr  36853  dfttc2g  36866  finxpreclem2  37884  poimirlem25  38144  mblfinlem4  38159  iscringd  38497  unichnidl  38530