internlm/Lean-Github huggingface dataset:
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') := context _ _ (by simp)
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s2 : {φ ∧' (φ →' ⊥')} ⊢ (φ ∧' (φ →' ⊥') →' φ) := by apply axiomEConj₁;
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s3 : {φ ∧' (φ →' ⊥')} ⊢ (φ ∧' (φ →' ⊥') →' (φ →' ⊥')) := by apply axiomEConj₂;
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s4 := MP s2 s1
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s5 := MP s3 s1
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
s5 : {φ ∧' (φ →' ⊥')} ⊢ φ →' ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
s5 : {φ ∧' (φ →' ⊥')} ⊢ φ →' ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s6 := MP s5 s4
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
s5 : {φ ∧' (φ →' ⊥')} ⊢ φ →' ⊥'
s6 : {φ ∧' (φ →' ⊥')} ⊢ ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
s5 : {φ ∧' (φ →' ⊥')} ⊢ φ →' ⊥'
s6 : {φ ∧' (φ →' ⊥')} ⊢ ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
⊢ φ ∧' (φ →' ⊥') ∈ {φ ∧' (φ →' ⊥')}
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
⊢ {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
Tactic:
apply axiomEConj₁
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof 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
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
Tactic:
apply axiomEConj₂
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm
Proof 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
φ ψ : L
⊢ ∅ ⊢ φ ∨' ψ →' ψ ∨' φ
Tactic:
simp [deduction]
Proof 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
φ ψ : L
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm
Proof 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
φ ψ : L
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Tactic:
have s1 : {φ ∨' ψ} ⊢ φ ∨' ψ := by simp;
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Tactic:
have s2 : {φ ∨' ψ} ⊢ φ →' (ψ ∨' φ) := by apply axiomIDisj₂;
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
s2 : {φ ∨' ψ} ⊢ φ →' ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
s2 : {φ ∨' ψ} ⊢ φ →' ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Tactic:
have s3 : {φ ∨' ψ} ⊢ ψ →' (ψ ∨' φ) := by apply axiomIDisj₁;
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
s2 : {φ ∨' ψ} ⊢ φ →' ψ ∨' φ
s3 : {φ ∨' ψ} ⊢ ψ →' ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
s2 : {φ ∨' ψ} ⊢ φ →' ψ ∨' φ
s3 : {φ ∨' ψ} ⊢ ψ →' ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Tactic:
have s5 := MP (EDisj s2 s3) s1
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
s2 : {φ ∨' ψ} ⊢ φ →' ψ ∨' φ
s3 : {φ ∨' ψ} ⊢ ψ →' ψ ∨' φ
s5 : {φ ∨' ψ} ⊢ ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
s2 : {φ ∨' ψ} ⊢ φ →' ψ ∨' φ
s3 : {φ ∨' ψ} ⊢ ψ →' ψ ∨' φ
s5 : {φ ∨' ψ} ⊢ ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm
Proof 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
φ ψ : L
⊢ {φ ∨' ψ} ⊢ φ ∨' ψ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
⊢ {φ ∨' ψ} ⊢ φ →' ψ ∨' φ
Tactic:
apply axiomIDisj₂
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm
Proof 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
φ ψ : L
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
s2 : {φ ∨' ψ} ⊢ φ →' ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ →' ψ ∨' φ
Tactic:
apply axiomIDisj₁
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.conjComm
Proof 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
φ ψ : L
⊢ ∅ ⊢ φ ∧' ψ →' ψ ∧' φ
Tactic:
simp [deduction]
Proof 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
φ ψ : L
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.conjComm
Proof 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
φ ψ : L
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Tactic:
have s1 : {φ ∧' ψ} ⊢ φ ∧' ψ := by simp;
Proof 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
φ ψ : L
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.conjComm
Proof 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
φ ψ : L
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Tactic:
have s2 := EConj₂ s1
Proof 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
φ ψ : L
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.conjComm
Proof 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
φ ψ : L
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Tactic:
have s3 := EConj₁ s1
Proof 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
φ ψ : L
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
s3 : {φ ∧' ψ} ⊢ φ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.conjComm
Proof 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
φ ψ : L
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
s3 : {φ ∧' ψ} ⊢ φ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Tactic:
have s6 := IConj s2 s3
Proof 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
φ ψ : L
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
s3 : {φ ∧' ψ} ⊢ φ
s6 : {φ ∧' ψ} ⊢ ψ ∧' φ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Theorem: PropositionalLogic.HilbertSystem.HPM.conjComm
Proof 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
φ ψ : L
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
s3 : {φ ∧' ψ} ⊢ φ
s6 : {φ ∧' ψ} ⊢ ψ ∧' φ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.conjComm
Proof 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
φ ψ : L
⊢ {φ ∧' ψ} ⊢ φ ∧' ψ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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:
simp [deduction]
Proof 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
⊢ (Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)) → (Γ ∪ {φ₁} ⊢ φ₂)
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₁} ⊢ φ₂
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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:
have s1 : Γ ∪ {φ₁} ⊢ φ₁ := by simp;
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
⊢ Γ ∪ {φ₁} ⊢ φ₂
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
⊢ Γ ∪ {φ₁} ⊢ φ₂
Tactic:
have s2 : Γ ∪ {φ₁} ⊢ ((φ₁ →' φ₂) ∧' (φ₂ →' φ₁)) →' (φ₁ →' φ₂) := by apply axiomEConj₁;
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
s2 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
⊢ Γ ∪ {φ₁} ⊢ φ₂
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
s2 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
⊢ Γ ∪ {φ₁} ⊢ φ₂
Tactic:
have s3 := weakenContext Γ (Γ ∪ {φ₁}) (by simp) h
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
s2 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
s3 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₁} ⊢ φ₂
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
s2 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
s3 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₁} ⊢ φ₂
Tactic:
have s4 := MP s2 s3
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
s2 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
s3 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s4 : Γ ∪ {φ₁} ⊢ φ₁ →' φ₂
⊢ Γ ∪ {φ₁} ⊢ φ₂
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
s2 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
s3 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s4 : Γ ∪ {φ₁} ⊢ φ₁ →' φ₂
⊢ Γ ∪ {φ₁} ⊢ φ₂
Tactic:
have s5 := MP s4 s1
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
s2 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
s3 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s4 : Γ ∪ {φ₁} ⊢ φ₁ →' φ₂
s5 : Γ ∪ {φ₁} ⊢ φ₂
⊢ Γ ∪ {φ₁} ⊢ φ₂
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
s2 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
s3 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s4 : Γ ∪ {φ₁} ⊢ φ₁ →' φ₂
s5 : Γ ∪ {φ₁} ⊢ φ₂
⊢ Γ ∪ {φ₁} ⊢ φ₂
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
⊢ Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
Tactic:
apply axiomEConj₁
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₁} ⊢ φ₁
s2 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
⊢ Γ ⊆ Γ ∪ {φ₁}
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mpr'
Proof 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:
simp [deduction]
Proof 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
⊢ (Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)) → (Γ ∪ {φ₂} ⊢ φ₁)
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mpr'
Proof 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
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₂} ⊢ φ₁
Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mpr'
Proof 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:
have s1 : Γ ∪ {φ₂} ⊢ φ₂ := by simp;
Proof 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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₂} ⊢ φ₂
⊢ Γ ∪ {φ₂} ⊢ φ₁