Theorem: LO.System.consistent_iff_unprovable_bot (Logic/Logic/System.lean)

State before:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
inst✝ : DeductiveExplosion S
𝓢 : S
⊢ Consistent 𝓢 ↔ 𝓢 ⊬! ⊥
Tactic:
simp [inconsistent_iff_provable_bot, ←not_inconsistent_iff_consistent]
State after:
no goals