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 | ⊢ ( ( 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → ∀ 𝑥 𝜓 ) → ( 𝜑 → ∀ 𝑥 𝜒 ) ) ) |