English
If for all a,b,c, p a b c implies q a b c, and for all a,b,c, p a b c holds, then for all a,b,c, q a b c holds.
Русский
Если для всех 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(\\\\forall a\\\\,\\\\forall b\\\\,\\\\forall c, p(a,b,c))\\\\rightarrow\\\\forall a\\\\,\\\\forall b\\\\,\\\\forall c, q(a,b,c)$$$
Lean4
theorem forall₃_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 :=
forall_imp fun a ↦ forall₂_imp <| h a
