Theorem an12s 647

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 643 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 643	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylbi 216	1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  anabsan2  672  oecl  8519  oaass  8544  odi  8562  oen0  8569  oeworde  8576  ltexprlem4  11016  iccshftr  13445  iccshftl  13447  iccdil  13449  icccntr  13451  ndvdsadd  16335  eulerthlem2  16697  neips  22546  tx1stc  23083  filuni  23318  ufldom  23395  isch3  30357  unoplin  31036  hmoplin  31058  adjlnop  31202  chirredlem2  31507  btwnconn1lem12  34900  btwnconn1  34903  finxpreclem2  36075  poimirlem25  36317  mblfinlem4  36332  iscringd  36671  unichnidl  36704