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  8455  oaass  8479  odi  8497  oen0  8504  oeworde  8511  ltexprlem4  10933  iccshftr  13389  iccshftl  13391  iccdil  13393  icccntr  13395  ndvdsadd  16321  eulerthlem2  16693  neips  22998  tx1stc  23535  filuni  23770  ufldom  23847  isch3  31185  unoplin  31864  hmoplin  31886  adjlnop  32030  chirredlem2  32335  btwnconn1lem12  36076  btwnconn1  36079  finxpreclem2  37368  poimirlem25  37629  mblfinlem4  37644  iscringd  37982  unichnidl  38015