apply Iff.intro
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r ↔ 𝓢 ⊢! p ⟶ q ⟶ r
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r → 𝓢 ⊢! p ⟶ q ⟶ r

case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r