Theorem bj-cbveximdlem 37103

Description: A lemma for alpha-renaming of variables bound by an existential quantifier. Hypothesis bj-cbveximdlem.nfth can be proved either from DV conditions as in bj-cbveximdv 37107 or from a nonfreeness condition and excom 2197 as in bj-cbveximd 37105. Hypothesis bj-cbveximdlem.denote is weaker than the corresponding hypothesis of ~ bj-cbveximd0 , and this proof is therefore a bit longer, not using bj-spime 37100 but bj-eximcom 37090. (Contributed by BJ, 12-Mar-2023.) Proof should not use 19.35 1898. (Proof modification is discouraged.)

Hypotheses

Ref	Expression
bj-cbveximdlem.nf0	⊢ (𝜑 → ∀𝑥𝜑)
bj-cbveximdlem.nf1	⊢ (𝜑 → ∀𝑦𝜑)
bj-cbveximdlem.nfch	⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))
bj-cbveximdlem.nfth	⊢ (𝜑 → (∃𝑥∃𝑦𝜃 → ∃𝑦𝜃))
bj-cbveximdlem.denote	⊢ (𝜑 → ∀𝑥∃𝑦𝜓)
bj-cbveximdlem.maj	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
bj-cbveximdlem	⊢ (𝜑 → (∃𝑥𝜒 → ∃𝑦𝜃))

Proof of Theorem bj-cbveximdlem

Step	Hyp	Ref	Expression
1		bj-cbveximdlem.nf0	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		bj-cbveximdlem.denote	. . . 4 ⊢ (𝜑 → ∀𝑥∃𝑦𝜓)
3		bj-cbveximdlem.nf1	. . . . . 6 ⊢ (𝜑 → ∀𝑦𝜑)
4		bj-cbveximdlem.maj	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
5	4	ex 416	. . . . . 6 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
6	3, 5	eximdh 1885	. . . . 5 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦(𝜒 → 𝜃)))
7	1, 6	alimdh 1838	. . . 4 ⊢ (𝜑 → (∀𝑥∃𝑦𝜓 → ∀𝑥∃𝑦(𝜒 → 𝜃)))
8	2, 7	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑥∃𝑦(𝜒 → 𝜃))
9		bj-cbveximdlem.nfth	. . 3 ⊢ (𝜑 → (∃𝑥∃𝑦𝜃 → ∃𝑦𝜃))
10		bj-eximcom 37090	. . 3 ⊢ (∃𝑦(𝜒 → 𝜃) → (∀𝑦𝜒 → ∃𝑦𝜃))
11	8, 9, 10	bj-exlimd 37081	. 2 ⊢ (𝜑 → (∃𝑥∀𝑦𝜒 → ∃𝑦𝜃))
12		bj-cbveximdlem.nfch	. 2 ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))
13	1, 11, 12	bj-exlimd 37081	1 ⊢ (𝜑 → (∃𝑥𝜒 → ∃𝑦𝜃))

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1559  ∃wex 1800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801

This theorem is referenced by:  bj-cbveximd  37105  bj-cbveximdv  37107