Theorem an12s 662

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anabsan2  687  oecl  8545  oaass  8569  odi  8587  oen0  8595  oeworde  8602  ltexprlem4  11124  iccshftr  13617  iccshftl  13619  iccdil  13621  icccntr  13623  ndvdsadd  16580  eulerthlem2  16959  neips  23431  tx1stc  23969  filuni  24204  ufldom  24281  isch3  31843  unoplin  32522  hmoplin  32544  adjlnop  32688  chirredlem2  32993  btwnconn1lem12  36863  btwnconn1  36866  ttctr  37281  dfttc2g  37294  finxpreclem2  38313  poimirlem25  38563  mblfinlem4  38578  iscringd  38932  unichnidl  38965