Theorem anim1 ≪ | index | src | ≫

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

(a -> b) -> a -> b

(a -> b) -> a /\ c -> b /\ c

Axiom use