theorem Ifeq1 (_p1 _p2: wff) (A B: set): $ (_p1 <-> _p2) -> If _p1 A B == If _p2 A B $;
(_p1 <-> _p2) -> (_p1 <-> _p2)
(_p1 <-> _p2) -> If _p1 A B == If _p2 A B