Metamath Proof Explorer


Theorem bisym1

Description: A symmetry with <-> .

See negsym1 for more information. (Contributed by Anthony Hart, 4-Sep-2011)

Ref Expression
Assertion bisym1
|- ( ( ps <-> ( ps <-> F. ) ) -> ( ps <-> ph ) )

Proof

Step Hyp Ref Expression
1 nbfal
 |-  ( -. ps <-> ( ps <-> F. ) )
2 1 bibi2i
 |-  ( ( ps <-> -. ps ) <-> ( ps <-> ( ps <-> F. ) ) )
3 pm5.19
 |-  -. ( ps <-> -. ps )
4 3 pm2.21i
 |-  ( ( ps <-> -. ps ) -> ( ps <-> ph ) )
5 2 4 sylbir
 |-  ( ( ps <-> ( ps <-> F. ) ) -> ( ps <-> ph ) )