Description: Stronger form of sylgt , closer to ax-2 . (Contributed by BJ, 30-Jul-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-sylggt | ⊢ ( ( 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → ∀ 𝑥 𝜓 ) → ( 𝜑 → ∀ 𝑥 𝜒 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alim | ⊢ ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) | |
2 | 1 | imim3i | ⊢ ( ( 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → ∀ 𝑥 𝜓 ) → ( 𝜑 → ∀ 𝑥 𝜒 ) ) ) |