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	|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ps /\ ( ph /\ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( ps /\ ch ) <-> ( ch /\ ps ) )
2	1	bianass	|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ch ) /\ ps ) )
3	2	biancomi	|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ps /\ ( ph /\ ch ) ) )