Description:luk-3 derived from the Tarski-Bernays-Wajsberg axioms.
This theorem, along with re1luk1 and re1luk2 proves that tbw-ax1 ,
tbw-ax2 , tbw-ax3 , and tbw-ax4 , with ax-mp can be used as a
complete axiom system for all of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011)(Proof modification is discouraged.)(New usage is discouraged.)