Metamath Proof Explorer

Theorem an21

Description: Swap two conjuncts. (Contributed by Peter Mazsa, 18-Sep-2022)

Ref Expression
Assertion an21 
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 biid 
 |-  ( ( ph /\ ch ) <-> ( ph /\ ch ) )
2 1 bianassc 
 |-  ( ( ps /\ ( ph /\ ch ) ) <-> ( ( ph /\ ps ) /\ ch ) )
3 2 bicomi 
 |-  ( ( ( ph /\ ps ) /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) )