Theorem ian ≪ | index | src | ≫ 

theorem ian (a b: wff): $ a -> b -> a /\ b $;
StepHypRefExpression
1 mpcom 
a -> (a -> ~b) -> ~b
2 1 con2d 
a -> b -> ~(a -> ~b)
3 2 conv an 
a -> b -> a /\ b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)