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  8478  oaass  8502  odi  8520  oen0  8527  oeworde  8534  ltexprlem4  10968  iccshftr  13423  iccshftl  13425  iccdil  13427  icccntr  13429  ndvdsadd  16356  eulerthlem2  16728  neips  23033  tx1stc  23570  filuni  23805  ufldom  23882  isch3  31220  unoplin  31899  hmoplin  31921  adjlnop  32065  chirredlem2  32370  btwnconn1lem12  36079  btwnconn1  36082  finxpreclem2  37371  poimirlem25  37632  mblfinlem4  37647  iscringd  37985  unichnidl  38018