:: deftheorem defines MP_rule PL_AXIOM:def 21 :
for p, q, r being Element of PL-WFF holds
( p,q MP_rule r iff q = p => r );