Theorem an12s 648

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 644 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 644	. 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  673  oecl  8593  oaass  8617  odi  8635  oen0  8642  oeworde  8649  ltexprlem4  11108  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  ndvdsadd  16458  eulerthlem2  16829  neips  23142  tx1stc  23679  filuni  23914  ufldom  23991  isch3  31273  unoplin  31952  hmoplin  31974  adjlnop  32118  chirredlem2  32423  btwnconn1lem12  36062  btwnconn1  36065  finxpreclem2  37356  poimirlem25  37605  mblfinlem4  37620  iscringd  37958  unichnidl  37991