Theorem an12s 661

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anabsan2  686  oecl  8518  oaass  8542  odi  8560  oen0  8568  oeworde  8575  ltexprlem4  11019  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  ndvdsadd  16463  eulerthlem2  16836  neips  23270  tx1stc  23807  filuni  24042  ufldom  24119  isch3  31593  unoplin  32272  hmoplin  32294  adjlnop  32438  chirredlem2  32743  btwnconn1lem12  36590  btwnconn1  36593  ttctr  37024  dfttc2g  37037  finxpreclem2  38056  poimirlem25  38316  mblfinlem4  38331  iscringd  38669  unichnidl  38702