Theorem bj-cbvalimdlem 37528

Description: A lemma for alpha-renaming of variables bound by a universal quantifier. Hypothesis bj-cbvalimdlem.nfch can be proved either from DV conditions as in bj-cbvalimdv 37532 or from a nonfreeness condition and alcom 2195 as in bj-cbvalimd 37530. Hypothesis bj-cbvalimdlem.denote is weaker than the corresponding hypothesis of bj-cbvalimd0 37527, and this proof is therefore a bit longer, not using bj-spim 37525 but bj-eximcom 37516. (Contributed by BJ, 12-Mar-2023.) Proof should not use 19.35 1909. (Proof modification is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
bj-cbvalimdlem	⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))

Proof of Theorem bj-cbvalimdlem

Step	Hyp	Ref	Expression
1		bj-cbvalimdlem.nf1	. 2 ⊢ (𝜑 → ∀𝑦𝜑)
2		bj-cbvalimdlem.denote	. . . 4 ⊢ (𝜑 → ∀𝑦∃𝑥𝜓)
3		bj-cbvalimdlem.nf0	. . . . . 6 ⊢ (𝜑 → ∀𝑥𝜑)
4		bj-cbvalimdlem.maj	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
5	4	ex 418	. . . . . 6 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
6	3, 5	eximdh 1896	. . . . 5 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥(𝜒 → 𝜃)))
7	1, 6	alimdh 1849	. . . 4 ⊢ (𝜑 → (∀𝑦∃𝑥𝜓 → ∀𝑦∃𝑥(𝜒 → 𝜃)))
8	2, 7	mpd 16	. . 3 ⊢ (𝜑 → ∀𝑦∃𝑥(𝜒 → 𝜃))
9		bj-cbvalimdlem.nfch	. . 3 ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦∀𝑥𝜒))
10		bj-eximcom 37516	. . 3 ⊢ (∃𝑥(𝜒 → 𝜃) → (∀𝑥𝜒 → ∃𝑥𝜃))
11	8, 9, 10	bj-alrimd 37495	. 2 ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦∃𝑥𝜃))
12		bj-cbvalimdlem.nfth	. 2 ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))
13	1, 11, 12	bj-alrimd 37495	1 ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  bj-cbvalimd  37530  bj-cbvalimdv  37532