theorem :: ZF_LANG1:26

for H being ZF-formula st H is conditional holds
the_consequent_of H = the_argument_of (the_right_argument_of (the_argument_of H))