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  8557  oaass  8581  odi  8599  oen0  8606  oeworde  8613  ltexprlem4  11061  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  ndvdsadd  16429  eulerthlem2  16801  neips  23067  tx1stc  23604  filuni  23839  ufldom  23916  isch3  31188  unoplin  31867  hmoplin  31889  adjlnop  32033  chirredlem2  32338  btwnconn1lem12  36058  btwnconn1  36061  finxpreclem2  37350  poimirlem25  37611  mblfinlem4  37626  iscringd  37964  unichnidl  37997