Theorem an12s 878

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  anabsan2  898  1stconst  7434  2ndconst  7435  oecl  7788  oaass  7812  odi  7830  oen0  7837  oeworde  7844  ltexprlem4  10073  iccshftr  12519  iccshftl  12521  iccdil  12523  icccntr  12525  ndvdsadd  15356  eulerthlem2  15709  neips  21139  tx1stc  21675  filuni  21910  ufldom  21987  isch3  28428  unoplin  29109  hmoplin  29131  adjlnop  29275  chirredlem2  29580  btwnconn1lem12  32532  btwnconn1  32535  finxpreclem2  33556  poimirlem25  33765  mblfinlem4  33780  iscringd  34128  unichnidl  34161