Theorem eqtru ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		itru	T.
2		id	(a <-> T.) -> (a <-> T.)
3	1, 2	mpbiri	(a <-> T.) -> a
4		id	a -> a
5	1	a1i	a -> T.
6	4, 5	bithd	a -> (a <-> T.)
7	3, 6	ibii	a <-> T. <-> a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru)