From [Graphics:submitted.nbgr231.gif] and [Graphics:submitted.nbgr232.gif] we obtain by modus ponens

[Graphics:submitted.nbgr233.gif] [Graphics:submitted.nbgr234.gif].

For proving [Graphics:submitted.nbgr235.gif], by [Graphics:submitted.nbgr236.gif], it suffices to prove

[Graphics:submitted.nbgr237.gif] [Graphics:submitted.nbgr238.gif].

We prove the individual conjunctive parts of [Graphics:submitted.nbgr239.gif]:

Proof of [Graphics:submitted.nbgr240.gif] [Graphics:submitted.nbgr241.gif]:

Formula [Graphics:submitted.nbgr242.gif] is proved because it is an instance of [Graphics:submitted.nbgr243.gif].

Proof of [Graphics:submitted.nbgr244.gif] [Graphics:submitted.nbgr245.gif]:

Formula [Graphics:submitted.nbgr246.gif] is true because it is identical to [Graphics:submitted.nbgr247.gif].