Theorem imimd ≪ | index | src | ≫

theorem imimd (a b c d e: wff):
  $ a -> b -> c $ >
  $ a -> d -> e $ >
  $ a -> (c -> d) -> b -> e $;

Step	Hyp	Ref	Expression
1		hyp h1	a -> b -> c
2	1	imim1d	a -> (c -> d) -> b -> d
3		hyp h2	a -> d -> e
4	3	imim2d	a -> (b -> d) -> b -> e
5	2, 4	syld	a -> (c -> d) -> b -> e

Axiom use

axs_prop_calc (ax_1, ax_2, ax_mp)