Metamath Proof Explorer

Theorem pm11.71

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

Ref Expression
Assertion pm11.71 ⊢ ∃ x φ ∧ ∃ y χ → ∀ x φ → ψ ∧ ∀ y χ → θ ↔ ∀ x ∀ y φ ∧ χ → ψ ∧ θ

Proof

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