Theorem ifpid ≪ | index | src | ≫

theorem ifpid (a p: wff): $ ifp p a a <-> a $;

Step	Hyp	Ref	Expression
1		ifppos	p -> (ifp p a a <-> a)
2		ifpneg	~p -> (ifp p a a <-> a)
3	1, 2	cases	ifp p a a <-> a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)