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

Metamath Proof Explorer

Theorem an12

Description: Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995) (Proof shortened by Peter Mazsa, 18-Sep-2022)

		Ref	Expression
	Assertion	an12	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) ↔ ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	⊢ ( ( 𝜓 ∧ 𝜒 ) ↔ ( 𝜒 ∧ 𝜓 ) )
2	1	bianass	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) )
3	2	biancomi	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) ↔ ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ) ) )