imp3

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Or.imp3

English

From a ∨ (b ∨ c) and implications a→d, b→e, c→f, derive d ∨ (e ∨ f).

Русский

Из a ∨ (b ∨ c) и импликаций a→d, b→e, c→f следует d ∨ (e ∨ f).

LaTeX

$$$a \\lor (b \\lor c) \\to (a \\to d) \\to (b \\to e) \\to (c \\to f) \\to d \\lor (e \\lor f)$$$

Lean4

theorem imp3 {d e c f : Prop} (had : a → d) (hbe : b → e) (hcf : c → f) : a ∨ b ∨ c → d ∨ e ∨ f :=
  Or.imp had <| Or.imp hbe hcf

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru