Theorem imnang

Quantified implication in terms of quantified negation of conjunction. (Contributed by BJ, 16-Jul-2021.)

Conclusion

\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \leftrightarrow \forall x \, \neg (\varphi \wedge \psi) \)

Proof

imnan

albii _