Theorem trud ≪ | index | src | ≫

theorem trud (a: wff): $ T. -> a $ > $ a $;

Step	Hyp	Ref	Expression
1		hyp h	T. -> a
2		itru	T.
3	1, 2	ax_mp	a

Axiom use

axs_prop_calc (ax_mp, itru)