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  8573  oaass  8597  odi  8615  oen0  8622  oeworde  8629  ltexprlem4  11076  iccshftr  13522  iccshftl  13524  iccdil  13526  icccntr  13528  ndvdsadd  16443  eulerthlem2  16815  neips  23136  tx1stc  23673  filuni  23908  ufldom  23985  isch3  31269  unoplin  31948  hmoplin  31970  adjlnop  32114  chirredlem2  32419  btwnconn1lem12  36079  btwnconn1  36082  finxpreclem2  37372  poimirlem25  37631  mblfinlem4  37646  iscringd  37984  unichnidl  38017