Theorem 19.33b
The antecedent provides a condition implying the converse of 19.33.
(Contributed by NM, 27-Mar-2004.) (Proof shortened by Andrew Salmon,
25-May-2011.) (Proof shortened by Wolf Lammen, 5-Jul-2014.)
Conclusion
\( \vdash \neg (\exists x \, \varphi \wedge \exists x \, \psi) \rightarrow (\forall x \, (\varphi \vee \psi) \leftrightarrow \forall x \, \varphi \vee \forall x \, \psi) \)
Proof
l0
ianor
\( \vdash \neg (\exists x \, \varphi \wedge \exists x \, \psi) \leftrightarrow \neg \exists x \, \varphi \vee \neg \exists x \, \psi \)
l1
alnex
\( \vdash \forall x \, \neg \varphi \leftrightarrow \neg \exists x \, \varphi \)
pm2.53
al2imi _
\( \vdash \forall x \, (\varphi \vee \psi) \rightarrow \forall x \, \neg \varphi \rightarrow \forall x \, \psi \)
l4
biimtrrid l1 _
\( \vdash \forall x \, (\varphi \vee \psi) \rightarrow \neg \exists x \, \varphi \rightarrow \forall x \, \psi \)
olc
\( \vdash \forall x \, \psi \rightarrow \forall x \, \varphi \vee \forall x \, \psi \)
l6
syl6com l4 _
19.30
orcomd _
l9
ord _
\( \vdash \forall x \, (\varphi \vee \psi) \rightarrow \neg \exists x \, \psi \rightarrow \forall x \, \varphi \)
orc
\( \vdash \forall x \, \varphi \rightarrow \forall x \, \varphi \vee \forall x \, \psi \)
syl6com l9 _
jaoi l6 _
\( \vdash \neg \exists x \, \varphi \vee \neg \exists x \, \psi \rightarrow \forall x \, (\varphi \vee \psi) \rightarrow \forall x \, \varphi \vee \forall x \, \psi \)
l13
sylbi l0 _
19.33
impbid1 l13 _