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  8583  oaass  8607  odi  8625  oen0  8633  oeworde  8640  ltexprlem4  11163  iccshftr  13657  iccshftl  13659  iccdil  13661  icccntr  13663  ndvdsadd  16624  eulerthlem2  17003  neips  23486  tx1stc  24024  filuni  24259  ufldom  24336  isch3  31900  unoplin  32579  hmoplin  32601  adjlnop  32745  chirredlem2  33050  btwnconn1lem12  37078  btwnconn1  37081  ttctr  37496  dfttc2g  37509  finxpreclem2  38581  poimirlem25  38831  mblfinlem4  38846  iscringd  39198  unichnidl  39231