Theorems · Theorem · logic and foundations

ite_and

∀ {α : Sort u_1} (P Q : Prop) [inst : Decidable P] (a b : α) [inst_1 : Decidable Q],
  (if P ∧ Q then a else b) = if P then if Q then a else b else b

Defined in

Mathlib.Logic.Basic

Cited by

14 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

DecidableDecidable