let p, q be MC-formula; :: thesis: ( |-_IPC p & |-_IPC q implies |-_IPC p '&' q )
assume A1: ( |-_IPC p & |-_IPC q ) ; :: thesis: |-_IPC p '&' q
|-_IPC p => (q => (p '&' q)) by Th32;
then |-_IPC q => (p '&' q) by A1, Th37;
hence |-_IPC p '&' q by A1, Th37; :: thesis: verum