Metamath Proof Explorer

Theorem bisaiaisb

Description: Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016)

Ref Expression
Assertion bisaiaisb 
|- ( ( ps <-> ph ) -> ( ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 bicom1 
 |-  ( ( ps <-> ph ) -> ( ph <-> ps ) )