Theorem an12s 650

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 646 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 646	. 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  675  oecl  8472  oaass  8496  odi  8514  oen0  8522  oeworde  8529  ltexprlem4  10962  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  ndvdsadd  16379  eulerthlem2  16752  neips  23078  tx1stc  23615  filuni  23850  ufldom  23927  isch3  31312  unoplin  31991  hmoplin  32013  adjlnop  32157  chirredlem2  32462  btwnconn1lem12  36280  btwnconn1  36283  ttctr  36675  dfttc2g  36688  finxpreclem2  37706  poimirlem25  37966  mblfinlem4  37981  iscringd  38319  unichnidl  38352