Theorem an32s

Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996)

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

Proof

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