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  8553  oaass  8577  odi  8595  oen0  8603  oeworde  8610  ltexprlem4  11131  iccshftr  13624  iccshftl  13626  iccdil  13628  icccntr  13630  ndvdsadd  16589  eulerthlem2  16968  neips  23440  tx1stc  23978  filuni  24213  ufldom  24290  isch3  31852  unoplin  32531  hmoplin  32553  adjlnop  32697  chirredlem2  33002  btwnconn1lem12  36987  btwnconn1  36990  ttctr  37405  dfttc2g  37418  finxpreclem2  38450  poimirlem25  38700  mblfinlem4  38715  iscringd  39069  unichnidl  39102