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  8504  oaass  8528  odi  8546  oen0  8553  oeworde  8560  ltexprlem4  10999  iccshftr  13454  iccshftl  13456  iccdil  13458  icccntr  13460  ndvdsadd  16387  eulerthlem2  16759  neips  23007  tx1stc  23544  filuni  23779  ufldom  23856  isch3  31177  unoplin  31856  hmoplin  31878  adjlnop  32022  chirredlem2  32327  btwnconn1lem12  36093  btwnconn1  36096  finxpreclem2  37385  poimirlem25  37646  mblfinlem4  37661  iscringd  37999  unichnidl  38032