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  30525  unoplin  31204  hmoplin  31226  adjlnop  31370  chirredlem2  31675  btwnconn1lem12  35101  btwnconn1  35104  finxpreclem2  36319  poimirlem25  36561  mblfinlem4  36576  iscringd  36914  unichnidl  36947