let F, G, H be ZF-formula; :: thesis: ( F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H )
assume A1: ( F is_subformula_of G & G is_subformula_of H ) ; :: thesis: F is_subformula_of H

now

assume F <> G ; :: thesis: F is_subformula_of H
then A2: F is_proper_subformula_of G by A1, Def41;

now

assume G <> H ; :: thesis: F is_subformula_of H
then G is_proper_subformula_of H by A1, Def41;
then F is_proper_subformula_of H by A2, Th85;
hence F is_subformula_of H by Def41; :: thesis: verum

end;

hence F is_subformula_of H by A1; :: thesis: verum

end;

hence F is_subformula_of H by A1; :: thesis: verum