T40
|- @x(Fx -> Gx) -> (@xFx -> @xGx)
T41
|- @x(Fx -> Gx) -> ($xFx -> $xGx)
T42
|- $x(Fx v Gx) <-> $xFx v $xGx
T43
|- @x(Fx & Gx) <-> @xFx & @xGx
T44
|- $x(Fx & Gx) -> $xFx & $xGx
T45
|- @xFx v @xGx -> @x(Fx v Gx)
T46
|- ($xFx -> $xGx) -> $x(Fx -> Gx)
T47
|- (@xFx -> @xGx) -> $x(Fx -> Gx)
T48
|- ~@x(Fx <-> Gx) v (@xFx <-> @xGx)
T49
|- ~@x(Fx <-> Gx) v ($xFx <-> $xGx)
T50
|- ~@x(P & Fx) <-> (P -> ~@xFx)
T51
|- ~$x(P & Fx) <-> (P -> ~$xFx)
T52
|- @x(P v Fx) <-> (~P -> @xFx)
T53
|- $x(P v Fx) <-> (~P -> $xFx)
T54
|- @x(Fx -> P) <-> ($xFx -> P)
T55
|- ~$x(Fx -> P) <-> ~(@xFx -> P)
T56
|- @x(Fx <-> P) -> (@xFx <-> P)
T57
|- @x(Fx <-> P) -> ($xFx <-> P)
T58
|- ($xFx <-> P) -> $x(Fx <-> P)
T59
|- (@xFx <-> P) -> $x(Fx <-> P)