Theorem an12s 648

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 644 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 644	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylbi 220	1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anabsan2  673  oecl  8145  oaass  8170  odi  8188  oen0  8195  oeworde  8202  ltexprlem4  10450  iccshftr  12864  iccshftl  12866  iccdil  12868  icccntr  12870  ndvdsadd  15751  eulerthlem2  16109  neips  21718  tx1stc  22255  filuni  22490  ufldom  22567  isch3  29024  unoplin  29703  hmoplin  29725  adjlnop  29869  chirredlem2  30174  btwnconn1lem12  33672  btwnconn1  33675  finxpreclem2  34807  poimirlem25  35082  mblfinlem4  35097  iscringd  35436  unichnidl  35469