Theorem Ifneg ≪ | index | src | ≫

theorem Ifneg (A B: set) (p: wff): $ ~p -> If p A B == B $;

~p -> (ifp p (n e. A) (n e. B) <-> n e. B)

~p -> {n | ifp p (n e. A) (n e. B)} == B

~p -> If p A B == B

Axiom use