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

Metamath Proof Explorer

Theorem bj-cbvalim

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

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

Proof

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