From [Graphics:submitted.nbgr32.gif] and [Graphics:submitted.nbgr33.gif] we obtain by inverse modus ponens

[Graphics:submitted.nbgr34.gif] [Graphics:submitted.nbgr35.gif].

Formula [Graphics:submitted.nbgr36.gif] is simplified to

[Graphics:submitted.nbgr37.gif] [Graphics:submitted.nbgr38.gif].

Formula [Graphics:submitted.nbgr39.gif] is true because it is identical to [Graphics:submitted.nbgr40.gif].