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
|- ( ( 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 ) ) )