Theorem anidm ≪ | index | src | ≫

theorem anidm (a: wff): $ a /\ a <-> a $;

Step	Hyp	Ref	Expression
1		anl	a /\ a -> a
2		id	a -> a
3	2, 2	iand	a -> a /\ a
4	1, 3	ibii	a /\ a <-> a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)