% Mizar problem: t60_rewrite1,rewrite1,1917,31 
fof(t60_rewrite1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r13_rewrite1(A,B,C)
         => r2_rewrite1(A,B,C) ) ) ),
    inference(mizar_bg_added,[status(thm)],[d27_rewrite1,t38_rewrite1,t46_rewrite1]),
    [file(rewrite1,t60_rewrite1)]).

fof(d27_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r13_rewrite1(A,B,C)
        <=> ( r8_rewrite1(A,B,C)
            & ~ r5_rewrite1(A,B,C) ) ) ) ),
    file(rewrite1,d27_rewrite1),
    []).

fof(t38_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( ( r5_rewrite1(A,B,C)
            | r6_rewrite1(A,B,C) )
         => r2_rewrite1(A,B,C) ) ) ),
    file(rewrite1,t38_rewrite1),
    []).

fof(t46_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r8_rewrite1(A,B,C)
         => r6_rewrite1(A,B,C) ) ) ),
    file(rewrite1,t46_rewrite1),
    []).