Theorem 19.43OLD
Obsolete proof of 19.43. Do not delete as it is referenced on the
[mmrecent.html] page and in [conventions-labels]. (Contributed by NM,
5-Aug-1993.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash \exists x \, (\varphi \vee \psi) \leftrightarrow \exists x \, \varphi \vee \exists x \, \psi \)
Proof
ioran
l1
albii _
\( \vdash \forall x \, \neg (\varphi \vee \psi) \leftrightarrow \forall x \, (\neg \varphi \wedge \neg \psi) \)
l2
19.26
\( \vdash \forall x \, (\neg \varphi \wedge \neg \psi) \leftrightarrow \forall x \, \neg \varphi \wedge \forall x \, \neg \psi \)
l3
alnex
alnex
anbi12i l3 _
\( \vdash \forall x \, \neg \varphi \wedge \forall x \, \neg \psi \leftrightarrow \neg \exists x \, \varphi \wedge \neg \exists x \, \psi \)
3bitri l1 l2 _
l7
notbii _
\( \vdash \neg \forall x \, \neg (\varphi \vee \psi) \leftrightarrow \neg (\neg \exists x \, \varphi \wedge \neg \exists x \, \psi) \)
l8
df-ex
\( \vdash \exists x \, (\varphi \vee \psi) \leftrightarrow \neg \forall x \, \neg (\varphi \vee \psi) \)
oran
\( \vdash \exists x \, \varphi \vee \exists x \, \psi \leftrightarrow \neg (\neg \exists x \, \varphi \wedge \neg \exists x \, \psi) \)
3bitr4i l7 l8 _