Theorems · Theorem · logic and foundations

if_congr

∀ {α : Sort u_1} {P Q : Prop} [inst : Decidable P] [inst_1 : Decidable Q] {x y u v : α},
  (P ↔ Q) → x = u → y = v → (if P then x else y) = if Q then u else v

Defined in

Mathlib.Logic.Basic

Cited by

12 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

DecidableDecidable