Theorem: LO.System.ModusPonens.mdp! (Logic/Logic/HilbertStyle/Basic.lean)

State before:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
p q : F
inst✝ : ModusPonens 𝓢
⊢ 𝓢 ⊢! p ⟶ q → 𝓢 ⊢! p → 𝓢 ⊢! q
Tactic:
rintro ⟨hpq⟩ ⟨hp⟩
State after:
case intro.intro
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
p q : F
inst✝ : ModusPonens 𝓢
hpq : 𝓢 ⊢ p ⟶ q
hp : 𝓢 ⊢ p
⊢ 𝓢 ⊢! q

State before:
case intro.intro
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
p q : F
inst✝ : ModusPonens 𝓢
hpq : 𝓢 ⊢ p ⟶ q
hp : 𝓢 ⊢ p
⊢ 𝓢 ⊢! q
Tactic:
exact ⟨hpq ⨀ hp⟩
State after:
no goals