 Basically, the phenomenon arises because both implications collapse, and then intuitionistic implication becomes classic. From the semantical point of view, it happens that the models of the fibred logic are Heyting algebras which are simultaneously Boolean algebras: evidently the algebras collapse to the Boolean ones. From the point of view of proof theory, the problem appears as a consequence of the metaproperty called Deduction Metatheorem (DMT): let \(\to_1\) and \(\to_2\) be the intuitionistic and the classical implications, respectively. Then   \[ \begin{array}{lll} \Gamma,\varphi\vdash\psi  &amp; \textrm{ iff }&amp;  \Gamma\vdash(\varphi\to_1\psi)\\ \Gamma,\varphi\vdash\psi  &amp; \textrm{ iff }&amp;  \Gamma\vdash(\varphi\to_2\psi)\\ \end{array} \]   Thus, the following argument applies (see Gabbay 1996b):   \[\begin{array}{ll} (\varphi\to_1\psi)\vdash(\varphi\to_1\psi) &amp;  \textrm{(Axiom)}\\ (\varphi\to_1\psi),\,\varphi\vdash\psi  &amp;  \textrm{(DMT for } \rightarrow_1) \\ (\varphi\to_1\psi)\vdash(\varphi\to_2\psi) &amp;  \textrm{(DMT for } \rightarrow_2) \\ \end{array} \]   A similar argument shows that \((\varphi\to_2\psi)\vdash(\varphi\to_1\psi)\). That is, classical and intuitionistic implications collapse in the combined logic.