This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ) ) → 𝜃 )