Theorem id | index | src |

theorem id (a: wff): $ a -> a $;
StepHypRefExpression
1 ax_1
a -> a -> a
2 ax_1
a -> (a -> a) -> a
3 1, 2 mpd
a -> a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_mp)