Theorem ian | index | src |

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

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)