Theorem: PropositionalLogic.HilbertSystem.HPM.IConj (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 (axiomIConj _ _ _) hφ) hψ
State after:
no goals