Theorem: PropositionalLogic.HilbertSystem.HPM.EConj₁ (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
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 : Γ ⊢ φ₁ ∧' φ₂
⊢ Γ ⊢ φ₁

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 : Γ ⊢ φ₁ ∧' φ₂
⊢ Γ ⊢ φ₁
Tactic:
exact MP (axiomEConj₁ _ _ _) h
State after:
no goals