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  8525  oaass  8549  odi  8567  oen0  8575  oeworde  8582  ltexprlem4  11049  iccshftr  13540  iccshftl  13542  iccdil  13544  icccntr  13546  ndvdsadd  16501  eulerthlem2  16874  neips  23339  tx1stc  23877  filuni  24112  ufldom  24189  isch3  31723  unoplin  32402  hmoplin  32424  adjlnop  32568  chirredlem2  32873  btwnconn1lem12  36679  btwnconn1  36682  ttctr  37113  dfttc2g  37126  finxpreclem2  38145  poimirlem25  38395  mblfinlem4  38410  iscringd  38749  unichnidl  38782