theorem Th24: :: MODAL_1:29

for A, B being MP-wff holds (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff