Theorem an12s 661

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  anabsan2  686  oecl  8522  oaass  8546  odi  8564  oen0  8572  oeworde  8579  ltexprlem4  11024  iccshftr  13513  iccshftl  13515  iccdil  13517  icccntr  13519  ndvdsadd  16468  eulerthlem2  16841  neips  23239  tx1stc  23776  filuni  24011  ufldom  24088  isch3  31534  unoplin  32213  hmoplin  32235  adjlnop  32379  chirredlem2  32684  btwnconn1lem12  36489  btwnconn1  36492  ttctr  36893  dfttc2g  36906  finxpreclem2  37924  poimirlem25  38184  mblfinlem4  38199  iscringd  38537  unichnidl  38570