Theorem: PropositionalLogic.HilbertSystem.HPM.EDisj (PropositionalLogic/HilbertSystem/HPM.lean)

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
χ φ ψ : L
⊢ (Γ ⊢ φ →' χ) → (Γ ⊢ ψ →' χ) → (Γ ⊢ φ ∨' ψ →' χ)
Tactic:
intro hφ hψ
State after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
χ φ ψ : L
hφ : Γ ⊢ φ →' χ
hψ : Γ ⊢ ψ →' χ
⊢ Γ ⊢ φ ∨' ψ →' χ

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
χ φ ψ : L
hφ : Γ ⊢ φ →' χ
hψ : Γ ⊢ ψ →' χ
⊢ Γ ⊢ φ ∨' ψ →' χ
Tactic:
exact MP (MP (axiomEDisj _ _ _ _) hφ) hψ
State after:
no goals