Theorem bisym1 32418

Description: A symmetry with <->.

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

Assertion

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

Proof of Theorem bisym1

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   F. wfal 1488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-tru 1486  df-fal 1489

This theorem is referenced by: (None)