:: deftheorem defaxpl2 defines axpl2 PL_AXIOM:def 23 :
for A being Element of PL-WFF holds
( A is axpl2 iff ex p, q, r being Element of PL-WFF st A = (p => (q => r)) => ((p => q) => (p => r)) );