∀x(P(x)⇒Q(x))⇒(∀xP(x)⇒∀xQ(x))
https://scrapbox.io/files/65f9550d54173a002623de26.svg
code:proof.tikz(tex)
\usepackage{fitch}
\usepackage{amsmath}
\begin{document}
$\Large\begin{nd}
\hypo {h} {\forall x(P(x)\implies Q(x))}
\open
\hypo {p} {\forall xP(x)}
\have {px} {P(x)} \Ae{p}
\have {pq} {P(x)\implies Q(x)} \Ae{h}
\have {qx} {Q(x)} \ie{px,pq}
\close
\have {q} {\forall xQ(x)} \Ai{qx}
\close
\have {e} {\forall xP(x)\implies\forall yQ(x)} \ii{p-q}
\end{nd}$
\end{document}