We prove [Graphics:submitted.nbgr3.gif] by natural deduction.

We prove [Graphics:submitted.nbgr4.gif] in both directions.

Direction from left to right:

We assume

[Graphics:submitted.nbgr5.gif] [Graphics:submitted.nbgr6.gif]

and show

[Graphics:submitted.nbgr7.gif] [Graphics:submitted.nbgr8.gif].

We prove [Graphics:submitted.nbgr9.gif] by the deduction rule.

We assume

[Graphics:submitted.nbgr10.gif] [Graphics:submitted.nbgr11.gif]

and show

[Graphics:submitted.nbgr12.gif] [Graphics:submitted.nbgr13.gif].

From [Graphics:submitted.nbgr14.gif] and [Graphics:submitted.nbgr15.gif] we obtain by inverse modus ponens

[Graphics:submitted.nbgr16.gif] [Graphics:submitted.nbgr17.gif].

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

[Graphics:submitted.nbgr19.gif] [Graphics:submitted.nbgr20.gif].

Formula [Graphics:submitted.nbgr21.gif] is true because it is identical to [Graphics:submitted.nbgr22.gif].

Direction from right to left: