let A be non empty Subset of GRZ-formula-set; :: thesis: for t, u being GRZ-formula st A, GRZ-rules |- t & A, GRZ-rules |- t => u holds
A, GRZ-rules |- u
let t, u be GRZ-formula; :: thesis: ( A, GRZ-rules |- t & A, GRZ-rules |- t => u implies A, GRZ-rules |- u )
assume that
A1: A, GRZ-rules |- t and
A2: A, GRZ-rules |- t => u ; :: thesis: A, GRZ-rules |- u
A, GRZ-rules |- t '&' u by A1, A2, Th61;
hence A, GRZ-rules |- u by Th60; :: thesis: verum