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