  We define a fragment of propositional logic where isomorphic propositions,
such as $A\land B$ and $B\land A$, or $A\Rightarrow (B\land C)$ and
$(A\Rightarrow B)\land(A\Rightarrow C)$ are identified. We define System I, a
proof language for this logic, and prove its normalisation and consistency.
