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  8501  oaass  8525  odi  8543  oen0  8550  oeworde  8557  ltexprlem4  10992  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  ndvdsadd  16380  eulerthlem2  16752  neips  23000  tx1stc  23537  filuni  23772  ufldom  23849  isch3  31170  unoplin  31849  hmoplin  31871  adjlnop  32015  chirredlem2  32320  btwnconn1lem12  36086  btwnconn1  36089  finxpreclem2  37378  poimirlem25  37639  mblfinlem4  37654  iscringd  37992  unichnidl  38025