pm11.71

		Ref	Expression
	Assertion	pm11.71	$⊢ (\exists x φ \land \exists y χ) \to ((\forall x (φ \to ψ) \land \forall y (χ \to θ)) \leftrightarrow \forall x \forall y ((φ \land χ) \to (ψ \land θ)))$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ y (φ \to ψ)$
2		nfv	$⊢ Ⅎ x (χ \to θ)$
3	1 2	aaan	$⊢ \forall x \forall y ((φ \to ψ) \land (χ \to θ)) \leftrightarrow (\forall x (φ \to ψ) \land \forall y (χ \to θ))$
4		anim12	$⊢ ((φ \to ψ) \land (χ \to θ)) \to ((φ \land χ) \to (ψ \land θ))$
5	4	2alimi	$⊢ \forall x \forall y ((φ \to ψ) \land (χ \to θ)) \to \forall x \forall y ((φ \land χ) \to (ψ \land θ))$
6	3 5	sylbir	$⊢ (\forall x (φ \to ψ) \land \forall y (χ \to θ)) \to \forall x \forall y ((φ \land χ) \to (ψ \land θ))$
7		nfv	$⊢ Ⅎ x χ$
8	7	nfex	$⊢ Ⅎ x \exists y χ$
9		exim	$⊢ \forall y ((φ \land χ) \to (ψ \land θ)) \to (\exists y (φ \land χ) \to \exists y (ψ \land θ))$
10		19.42v	$⊢ \exists y (φ \land χ) \leftrightarrow (φ \land \exists y χ)$
11		19.42v	$⊢ \exists y (ψ \land θ) \leftrightarrow (ψ \land \exists y θ)$
12	9 10 11	3imtr3g	$⊢ \forall y ((φ \land χ) \to (ψ \land θ)) \to ((φ \land \exists y χ) \to (ψ \land \exists y θ))$
13		pm3.21	$⊢ \exists y χ \to (φ \to (φ \land \exists y χ))$
14		simpl	$⊢ (ψ \land \exists y θ) \to ψ$
15	14	imim2i	$⊢ ((φ \land \exists y χ) \to (ψ \land \exists y θ)) \to ((φ \land \exists y χ) \to ψ)$
16	13 15	syl9	$⊢ \exists y χ \to (((φ \land \exists y χ) \to (ψ \land \exists y θ)) \to (φ \to ψ))$
17	12 16	syl5	$⊢ \exists y χ \to (\forall y ((φ \land χ) \to (ψ \land θ)) \to (φ \to ψ))$
18	8 17	alimd	$⊢ \exists y χ \to (\forall x \forall y ((φ \land χ) \to (ψ \land θ)) \to \forall x (φ \to ψ))$
19	18	adantl	$⊢ (\exists x φ \land \exists y χ) \to (\forall x \forall y ((φ \land χ) \to (ψ \land θ)) \to \forall x (φ \to ψ))$
20		ax-11	$⊢ \forall x \forall y ((φ \land χ) \to (ψ \land θ)) \to \forall y \forall x ((φ \land χ) \to (ψ \land θ))$
21		nfv	$⊢ Ⅎ y φ$
22	21	nfex	$⊢ Ⅎ y \exists x φ$
23		exim	$⊢ \forall x ((φ \land χ) \to (ψ \land θ)) \to (\exists x (φ \land χ) \to \exists x (ψ \land θ))$
24		19.41v	$⊢ \exists x (φ \land χ) \leftrightarrow (\exists x φ \land χ)$
25		19.41v	$⊢ \exists x (ψ \land θ) \leftrightarrow (\exists x ψ \land θ)$
26	23 24 25	3imtr3g	$⊢ \forall x ((φ \land χ) \to (ψ \land θ)) \to ((\exists x φ \land χ) \to (\exists x ψ \land θ))$
27		pm3.2	$⊢ \exists x φ \to (χ \to (\exists x φ \land χ))$
28		simpr	$⊢ (\exists x ψ \land θ) \to θ$
29	28	imim2i	$⊢ ((\exists x φ \land χ) \to (\exists x ψ \land θ)) \to ((\exists x φ \land χ) \to θ)$
30	27 29	syl9	$⊢ \exists x φ \to (((\exists x φ \land χ) \to (\exists x ψ \land θ)) \to (χ \to θ))$
31	26 30	syl5	$⊢ \exists x φ \to (\forall x ((φ \land χ) \to (ψ \land θ)) \to (χ \to θ))$
32	22 31	alimd	$⊢ \exists x φ \to (\forall y \forall x ((φ \land χ) \to (ψ \land θ)) \to \forall y (χ \to θ))$
33	20 32	syl5	$⊢ \exists x φ \to (\forall x \forall y ((φ \land χ) \to (ψ \land θ)) \to \forall y (χ \to θ))$
34	33	adantr	$⊢ (\exists x φ \land \exists y χ) \to (\forall x \forall y ((φ \land χ) \to (ψ \land θ)) \to \forall y (χ \to θ))$
35	19 34	jcad	$⊢ (\exists x φ \land \exists y χ) \to (\forall x \forall y ((φ \land χ) \to (ψ \land θ)) \to (\forall x (φ \to ψ) \land \forall y (χ \to θ)))$
36	6 35	impbid2	$⊢ (\exists x φ \land \exists y χ) \to ((\forall x (φ \to ψ) \land \forall y (χ \to θ)) \leftrightarrow \forall x \forall y ((φ \land χ) \to (ψ \land θ)))$

Metamath Proof Explorer

Theorem pm11.71

Proof