Theorem an12s

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 is combined with syl (or a variant). (Contributed by NM, 13-Mar-1996)

	Ref	Expression
Hypothesis	an12s.1	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝜃 )
Assertion	an12s	⊢ ( ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ) ) → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		an12s.1	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝜃 )
2		an12	⊢ ( ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ) ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) )
3	2 1	sylbi	⊢ ( ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ) ) → 𝜃 )