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 ψψψφ

Proof

Step Hyp Ref Expression
1 nbfal ¬ψψ
2 1 bibi2i ψ¬ψψψ
3 pm5.19 ¬ψ¬ψ
4 3 pm2.21i ψ¬ψψφ
5 2 4 sylbir ψψψφ