theorem monmp: :: PL_AXIOM:55

for p being Element of PL-WFF
for F, G being Subset of PL-WFF st F c= G & F |- p holds
G |- p