Theorem pm11.71

Description: Theorem *11.71 in WhiteheadRussell p. 166. (Contributed by Andrew Salmon, 24-May-2011)

	Ref	Expression
Assertion	pm11.71	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜒 ) → ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ( 𝜒 → 𝜃 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑦 ( 𝜑 → 𝜓 )
2		nfv	⊢ Ⅎ 𝑥 ( 𝜒 → 𝜃 )
3	1 2	aaan	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 → 𝜓 ) ∧ ( 𝜒 → 𝜃 ) ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ( 𝜒 → 𝜃 ) ) )
4		anim12	⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( 𝜒 → 𝜃 ) ) → ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) )
5	4	2alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 → 𝜓 ) ∧ ( 𝜒 → 𝜃 ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) )
6	3 5	sylbir	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ( 𝜒 → 𝜃 ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) )
7		nfv	⊢ Ⅎ 𝑥 𝜒
8	7	nfex	⊢ Ⅎ 𝑥 ∃ 𝑦 𝜒
9		exim	⊢ ( ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ( ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) → ∃ 𝑦 ( 𝜓 ∧ 𝜃 ) ) )
10		19.42v	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜑 ∧ ∃ 𝑦 𝜒 ) )
11		19.42v	⊢ ( ∃ 𝑦 ( 𝜓 ∧ 𝜃 ) ↔ ( 𝜓 ∧ ∃ 𝑦 𝜃 ) )
12	9 10 11	3imtr3g	⊢ ( ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ( ( 𝜑 ∧ ∃ 𝑦 𝜒 ) → ( 𝜓 ∧ ∃ 𝑦 𝜃 ) ) )
13		pm3.21	⊢ ( ∃ 𝑦 𝜒 → ( 𝜑 → ( 𝜑 ∧ ∃ 𝑦 𝜒 ) ) )
14		simpl	⊢ ( ( 𝜓 ∧ ∃ 𝑦 𝜃 ) → 𝜓 )
15	14	imim2i	⊢ ( ( ( 𝜑 ∧ ∃ 𝑦 𝜒 ) → ( 𝜓 ∧ ∃ 𝑦 𝜃 ) ) → ( ( 𝜑 ∧ ∃ 𝑦 𝜒 ) → 𝜓 ) )
16	13 15	syl9	⊢ ( ∃ 𝑦 𝜒 → ( ( ( 𝜑 ∧ ∃ 𝑦 𝜒 ) → ( 𝜓 ∧ ∃ 𝑦 𝜃 ) ) → ( 𝜑 → 𝜓 ) ) )
17	12 16	syl5	⊢ ( ∃ 𝑦 𝜒 → ( ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ( 𝜑 → 𝜓 ) ) )
18	8 17	alimd	⊢ ( ∃ 𝑦 𝜒 → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
19	18	adantl	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜒 ) → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
20		ax-11	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ∀ 𝑦 ∀ 𝑥 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) )
21		nfv	⊢ Ⅎ 𝑦 𝜑
22	21	nfex	⊢ Ⅎ 𝑦 ∃ 𝑥 𝜑
23		exim	⊢ ( ∀ 𝑥 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) → ∃ 𝑥 ( 𝜓 ∧ 𝜃 ) ) )
24		19.41v	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ↔ ( ∃ 𝑥 𝜑 ∧ 𝜒 ) )
25		19.41v	⊢ ( ∃ 𝑥 ( 𝜓 ∧ 𝜃 ) ↔ ( ∃ 𝑥 𝜓 ∧ 𝜃 ) )
26	23 24 25	3imtr3g	⊢ ( ∀ 𝑥 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ( ( ∃ 𝑥 𝜑 ∧ 𝜒 ) → ( ∃ 𝑥 𝜓 ∧ 𝜃 ) ) )
27		pm3.2	⊢ ( ∃ 𝑥 𝜑 → ( 𝜒 → ( ∃ 𝑥 𝜑 ∧ 𝜒 ) ) )
28		simpr	⊢ ( ( ∃ 𝑥 𝜓 ∧ 𝜃 ) → 𝜃 )
29	28	imim2i	⊢ ( ( ( ∃ 𝑥 𝜑 ∧ 𝜒 ) → ( ∃ 𝑥 𝜓 ∧ 𝜃 ) ) → ( ( ∃ 𝑥 𝜑 ∧ 𝜒 ) → 𝜃 ) )
30	27 29	syl9	⊢ ( ∃ 𝑥 𝜑 → ( ( ( ∃ 𝑥 𝜑 ∧ 𝜒 ) → ( ∃ 𝑥 𝜓 ∧ 𝜃 ) ) → ( 𝜒 → 𝜃 ) ) )
31	26 30	syl5	⊢ ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ( 𝜒 → 𝜃 ) ) )
32	22 31	alimd	⊢ ( ∃ 𝑥 𝜑 → ( ∀ 𝑦 ∀ 𝑥 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ∀ 𝑦 ( 𝜒 → 𝜃 ) ) )
33	20 32	syl5	⊢ ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ∀ 𝑦 ( 𝜒 → 𝜃 ) ) )
34	33	adantr	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜒 ) → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ∀ 𝑦 ( 𝜒 → 𝜃 ) ) )
35	19 34	jcad	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜒 ) → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ( 𝜒 → 𝜃 ) ) ) )
36	6 35	impbid2	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜒 ) → ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ( 𝜒 → 𝜃 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜃 ) ) ) )