English
If for all a,b,c, p a b c implies q a b c, and there exists a,b,c with p a b c, then there exists a,b,c with q a b c.
Русский
Если для всех a,b,c верно p(a,b,c)→q(a,b,c), и существует a,b,c с p(a,b,c), то существует a,b,c с q(a,b,c).
LaTeX
$$$(\\\\forall a\\\\,\\\\forall b\\\\,\\\\forall c, p(a,b,c)\\\\rightarrow q(a,b,c))\\\\rightarrow(\\\\exists a\\\\,\\\\exists b\\\\,\\\\exists c, p(a,b,c))\\\\rightarrow\\\\exists a\\\\,\\\\exists b\\\\,\\\\exists c, q(a,b,c)$$$
Lean4
theorem imp {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c → q a b c) : (∃ a b c, p a b c) → ∃ a b c, q a b c :=
Exists.imp fun a ↦ Exists₂.imp <| h a
