Theorem an12s 649

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 645 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 645	. 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  674  oecl  8549  oaass  8573  odi  8591  oen0  8598  oeworde  8605  ltexprlem4  11053  iccshftr  13503  iccshftl  13505  iccdil  13507  icccntr  13509  ndvdsadd  16429  eulerthlem2  16801  neips  23051  tx1stc  23588  filuni  23823  ufldom  23900  isch3  31222  unoplin  31901  hmoplin  31923  adjlnop  32067  chirredlem2  32372  btwnconn1lem12  36116  btwnconn1  36119  finxpreclem2  37408  poimirlem25  37669  mblfinlem4  37684  iscringd  38022  unichnidl  38055