iff_assoc — Mathlib

English

For any propositions a, b, c, the associativity of the if-and-only-if connective holds: ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c)).

Русский

Для любых высказываний a, b, c выполняется ассоциативность двоичного эквивалентности: ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c)).

LaTeX

$$$ ((a \leftrightarrow b) \leftrightarrow c) \leftrightarrow (a \leftrightarrow (b \leftrightarrow c)) $$$

Lean4

theorem iff_assoc {a b c : Prop} : ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c)) := by tauto

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