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  8528  oaass  8552  odi  8570  oen0  8578  oeworde  8585  ltexprlem4  11041  iccshftr  13531  iccshftl  13533  iccdil  13535  icccntr  13537  ndvdsadd  16492  eulerthlem2  16865  neips  23322  tx1stc  23860  filuni  24095  ufldom  24172  isch3  31666  unoplin  32345  hmoplin  32367  adjlnop  32511  chirredlem2  32816  btwnconn1lem12  36629  btwnconn1  36632  ttctr  37063  dfttc2g  37076  finxpreclem2  38095  poimirlem25  38355  mblfinlem4  38370  iscringd  38709  unichnidl  38742