Theorem nfald
Deduction form of nfal. (Contributed by Mario Carneiro,
24-Sep-2016.) (Proof shortened by Wolf Lammen, 16-Oct-2021.)
Hypotheses
nfald.1
\( \vdash \Finv y \, \varphi \)
nfald.2
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \forall y \, \psi \)
Proof
l0
19.12
\( \vdash \exists x \, \forall y \, \psi \rightarrow \forall y \, \exists x \, \psi \)
l1
nfald.1
nfald.2
nfrd _
l4
alimd l1 _
\( \vdash \varphi \rightarrow \forall y \, \exists x \, \psi \rightarrow \forall y \, \forall x \, \psi \)
ax-11
\( \vdash \forall y \, \forall x \, \psi \rightarrow \forall x \, \forall y \, \psi \)
syl56 l0 l4 _
nfd _