theorem Th23: :: INTPRO_1:23

for p, q, r being Element of MC-wff st p => (q => r) in IPC-Taut holds
q => (p => r) in IPC-Taut