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  8462  oaass  8486  odi  8504  oen0  8512  oeworde  8519  ltexprlem4  10948  iccshftr  13400  iccshftl  13402  iccdil  13404  icccntr  13406  ndvdsadd  16335  eulerthlem2  16707  neips  23055  tx1stc  23592  filuni  23827  ufldom  23904  isch3  31265  unoplin  31944  hmoplin  31966  adjlnop  32110  chirredlem2  32415  btwnconn1lem12  36241  btwnconn1  36244  finxpreclem2  37534  poimirlem25  37785  mblfinlem4  37800  iscringd  38138  unichnidl  38171