Theorem an12s 662

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anabsan2  687  oecl  8546  oaass  8570  odi  8588  oen0  8596  oeworde  8603  ltexprlem4  11125  iccshftr  13618  iccshftl  13620  iccdil  13622  icccntr  13624  ndvdsadd  16581  eulerthlem2  16960  neips  23432  tx1stc  23970  filuni  24205  ufldom  24282  isch3  31844  unoplin  32523  hmoplin  32545  adjlnop  32689  chirredlem2  32994  btwnconn1lem12  36938  btwnconn1  36941  ttctr  37356  dfttc2g  37369  finxpreclem2  38389  poimirlem25  38639  mblfinlem4  38654  iscringd  39008  unichnidl  39041