that exists because any proof of formula_90 from the premise formula_38 can be converted into a proof of formula_92 from the premise formula_5 by doing an extra implication introduction step, and conversely any proof of formula_92 from the premise formula_5 can be converted into a proof of formula_90 from the premise formula_38 by doing an extra implication elimination step. Left-continuity of the t-norm is the necessary and sufficient condition for this relationship between a t-norm conjunction and its residual implication to hold.