This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-cbvexim

Description: A lemma used to prove bj-cbvex in a weak axiomatization. (Contributed by BJ, 12-Mar-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-cbvexim ( ∀ 𝑥 ∃ 𝑦 𝜒 → ( ∀ 𝑥 ∀ 𝑦 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 ax5e ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜓 → ∃ 𝑦 𝜓 )
2 ax-5 ⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
3 2 ax-gen ⊢ ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 )
4 bj-cbveximt ⊢ ( ∀ 𝑥 ∃ 𝑦 𝜒 → ( ∀ 𝑥 ∀ 𝑦 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 ) → ( ( ∃ 𝑥 ∃ 𝑦 𝜓 → ∃ 𝑦 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 ) ) ) ) )
5 4 com3l ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 ) → ( ∀ 𝑥 ∃ 𝑦 𝜒 → ( ( ∃ 𝑥 ∃ 𝑦 𝜓 → ∃ 𝑦 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 ) ) ) ) )
6 5 com14 ⊢ ( ( ∃ 𝑥 ∃ 𝑦 𝜓 → ∃ 𝑦 𝜓 ) → ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 ) → ( ∀ 𝑥 ∃ 𝑦 𝜒 → ( ∀ 𝑥 ∀ 𝑦 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 ) ) ) ) )
7 1 3 6 mp2 ⊢ ( ∀ 𝑥 ∃ 𝑦 𝜒 → ( ∀ 𝑥 ∀ 𝑦 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 ) ) )