Theorem iand | index | src |

theorem iand (a b c: wff): $ a -> b $ > $ a -> c $ > $ a -> b /\ c $;
StepHypRefExpression
1 ian
b -> c -> b /\ c
2 hyp h1
a -> b
3 hyp h2
a -> c
4 1, 2, 3 sylc
a -> b /\ c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)