  Looking at the rules of conjunction and implication, one notes that  the premisses (the formulas immediately above the inference line) are subformulas of the conclusion in the I-rules, whereas it is the other way around in the E-rules. Gentzen noticed that in normal  derivations, this property of single steps is inherited by the whole  derivation, in the sense that all formulas are subformulas of the  conclusion. This result gave as a byproduct a decision method for   intuitionistic propositional logic.  Another corollary was a syntactic proof of consistency: if a  contradiction is provable, anything is provable, but an atomic  formula, say, has no proof: if it has a proof, it has a normal proof, but no E-rules apply to an atomic formula, and no I-rule concludes it either.