Theorem anim1a ≪ | index | src | ≫

theorem anim1a (a b c: wff): $ (a -> b -> c) -> b /\ a -> c /\ a $;

Step	Hyp	Ref	Expression
1		ancom	a /\ c -> c /\ a
2		ancom	b /\ a -> a /\ b
3		anim2a	(a -> b -> c) -> a /\ b -> a /\ c
4	2, 3	syl5	(a -> b -> c) -> b /\ a -> a /\ c
5	1, 4	syl6	(a -> b -> c) -> b /\ a -> c /\ a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)