theorem expd (a b c d: wff): $ a -> b /\ c -> d $ > $ a -> b -> c -> d $;
b /\ c -> d <-> b -> c -> d
a -> b /\ c -> d
a -> b -> c -> d