Theorem an12s 639

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  anabsan2  664  oecl  7901  oaass  7925  odi  7943  oen0  7950  oeworde  7957  ltexprlem4  10196  iccshftr  12623  iccshftl  12625  iccdil  12627  icccntr  12629  ndvdsadd  15540  eulerthlem2  15891  neips  21325  tx1stc  21862  filuni  22097  ufldom  22174  isch3  28670  unoplin  29351  hmoplin  29373  adjlnop  29517  chirredlem2  29822  btwnconn1lem12  32794  btwnconn1  32797  finxpreclem2  33822  poimirlem25  34060  mblfinlem4  34075  iscringd  34421  unichnidl  34454