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  8452  oaass  8476  odi  8494  oen0  8501  oeworde  8508  ltexprlem4  10930  iccshftr  13386  iccshftl  13388  iccdil  13390  icccntr  13392  ndvdsadd  16321  eulerthlem2  16693  neips  23028  tx1stc  23565  filuni  23800  ufldom  23877  isch3  31221  unoplin  31900  hmoplin  31922  adjlnop  32066  chirredlem2  32371  btwnconn1lem12  36142  btwnconn1  36145  finxpreclem2  37434  poimirlem25  37695  mblfinlem4  37710  iscringd  38048  unichnidl  38081