diff --git a/Mathlib/Data/List/TFAE.lean b/Mathlib/Data/List/TFAE.lean
index a102741f89bab2..6394c303df8d37 100644
--- a/Mathlib/Data/List/TFAE.lean
+++ b/Mathlib/Data/List/TFAE.lean
@@ -114,4 +114,11 @@ theorem exists_tfae {α : Type*} (l : List (α → Prop)) (H : ∀ a : α, (l.ma
   exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem (fun p ↦ p a) hp₁)
     (p₂ a) (mem_map_of_mem (fun p ↦ p a) hp₂)
 
+theorem tfae_not_iff {l : List Prop} : TFAE (l.map Not) ↔ TFAE l := by
+  classical
+  simp only [TFAE, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
+    Decidable.not_iff_not]
+
+alias ⟨_, TFAE.not⟩ := tfae_not_iff
+
 end List