Theorem 19.33b

Description: 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)

	Ref	Expression
Assertion	19.33b	$$⊢\neg \left(\exists x\phi \wedge \exists x\psi \right)\to \left(\forall x\left(\phi \vee \psi \right)\leftrightarrow \left(\forall x\phi \vee \forall x\psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ianor	$$⊢\neg \left(\exists x\phi \wedge \exists x\psi \right)\leftrightarrow \left(\neg \exists x\phi \vee \neg \exists x\psi \right)$$
2		alnex	$$⊢\forall x\neg \phi \leftrightarrow \neg \exists x\phi$$
3		pm2.53	$$⊢\left(\phi \vee \psi \right)\to \left(\neg \phi \to \psi \right)$$
4	3	al2imi	$$⊢\forall x\left(\phi \vee \psi \right)\to \left(\forall x\neg \phi \to \forall x\psi \right)$$
5	2 4	biimtrrid	$$⊢\forall x\left(\phi \vee \psi \right)\to \left(\neg \exists x\phi \to \forall x\psi \right)$$
6		olc	$$⊢\forall x\psi \to \left(\forall x\phi \vee \forall x\psi \right)$$
7	5 6	syl6com	$$⊢\neg \exists x\phi \to \left(\forall x\left(\phi \vee \psi \right)\to \left(\forall x\phi \vee \forall x\psi \right)\right)$$
8		19.30	$$⊢\forall x\left(\phi \vee \psi \right)\to \left(\forall x\phi \vee \exists x\psi \right)$$
9	8	orcomd	$$⊢\forall x\left(\phi \vee \psi \right)\to \left(\exists x\psi \vee \forall x\phi \right)$$
10	9	ord	$$⊢\forall x\left(\phi \vee \psi \right)\to \left(\neg \exists x\psi \to \forall x\phi \right)$$
11		orc	$$⊢\forall x\phi \to \left(\forall x\phi \vee \forall x\psi \right)$$
12	10 11	syl6com	$$⊢\neg \exists x\psi \to \left(\forall x\left(\phi \vee \psi \right)\to \left(\forall x\phi \vee \forall x\psi \right)\right)$$
13	7 12	jaoi	$$⊢\left(\neg \exists x\phi \vee \neg \exists x\psi \right)\to \left(\forall x\left(\phi \vee \psi \right)\to \left(\forall x\phi \vee \forall x\psi \right)\right)$$
14	1 13	sylbi	$$⊢\neg \left(\exists x\phi \wedge \exists x\psi \right)\to \left(\forall x\left(\phi \vee \psi \right)\to \left(\forall x\phi \vee \forall x\psi \right)\right)$$
15		19.33	$$⊢\left(\forall x\phi \vee \forall x\psi \right)\to \forall x\left(\phi \vee \psi \right)$$
16	14 15	impbid1	$$⊢\neg \left(\exists x\phi \wedge \exists x\psi \right)\to \left(\forall x\left(\phi \vee \psi \right)\leftrightarrow \left(\forall x\phi \vee \forall x\psi \right)\right)$$