let p, q, s be Element of HP-WFF ; :: thesis: ( s => (q => p) in HP_TAUT & q in HP_TAUT implies s => p in HP_TAUT )
assume that
A1: s => (q => p) in HP_TAUT and
A2: q in HP_TAUT ; :: thesis: s => p in HP_TAUT
(s => (q => p)) => (q => (s => p)) in HP_TAUT by Th26;
then q => (s => p) in HP_TAUT by A1, Def10;
hence s => p in HP_TAUT by A2, Def10; :: thesis: verum