apply Iff.intro
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ ↔ lindenbaumExtension t Δ⊢f
case mp
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ → lindenbaumExtension t Δ⊢f

case mpr
t : Th
Δ : Ctx
f : Form
⊢ lindenbaumExtension t Δ⊢f → f ∈ lindenbaumExtension t Δ