Theorem an12s 646

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 642 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 642	. 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  671  oecl  8367  oaass  8392  odi  8410  oen0  8417  oeworde  8424  ltexprlem4  10795  iccshftr  13218  iccshftl  13220  iccdil  13222  icccntr  13224  ndvdsadd  16119  eulerthlem2  16483  neips  22264  tx1stc  22801  filuni  23036  ufldom  23113  isch3  29603  unoplin  30282  hmoplin  30304  adjlnop  30448  chirredlem2  30753  btwnconn1lem12  34400  btwnconn1  34403  finxpreclem2  35561  poimirlem25  35802  mblfinlem4  35817  iscringd  36156  unichnidl  36189