% Mizar problem: t43_rewrite1,rewrite1,870,29 
fof(t43_rewrite1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C,D] : 
          ( ( ( r1_rewrite1(A,B,C)
              & r5_rewrite1(A,C,D) )
            | ( r5_rewrite1(A,B,C)
              & r1_rewrite1(A,D,C) ) )
         => r5_rewrite1(A,B,D) ) ) ),
    inference(mizar_bg_added,[status(thm)],[d7_rewrite1,t17_rewrite1]),
    [file(rewrite1,t43_rewrite1)]).

fof(d7_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r5_rewrite1(A,B,C)
        <=> ? [D] : 
              ( r1_rewrite1(A,B,D)
              & r1_rewrite1(A,C,D) ) ) ) ),
    file(rewrite1,d7_rewrite1),
    []).

fof(t17_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C,D] : 
          ( ( r1_rewrite1(A,B,C)
            & r1_rewrite1(A,C,D) )
         => r1_rewrite1(A,B,D) ) ) ),
    file(rewrite1,t17_rewrite1),
    []).