Theorem an12s 648

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anabsan2  673  oecl  8537  oaass  8561  odi  8579  oen0  8586  oeworde  8593  ltexprlem4  11034  iccshftr  13463  iccshftl  13465  iccdil  13467  icccntr  13469  ndvdsadd  16353  eulerthlem2  16715  neips  22617  tx1stc  23154  filuni  23389  ufldom  23466  isch3  30494  unoplin  31173  hmoplin  31195  adjlnop  31339  chirredlem2  31644  btwnconn1lem12  35070  btwnconn1  35073  finxpreclem2  36271  poimirlem25  36513  mblfinlem4  36528  iscringd  36866  unichnidl  36899