internlm/Lean-Github huggingface dataset:
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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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_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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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_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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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_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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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_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 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₂} ⊢ φ₂
s2 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₂ →' φ₁
s3 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s4 : Γ ∪ {φ₂} ⊢ φ₂ →' φ₁
s5 : Γ ∪ {φ₂} ⊢ φ₁
⊢ Γ ∪ {φ₂} ⊢ φ₁
Tactic:
assumption
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
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₂} ⊢ φ₂
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
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₂} ⊢ φ₂
⊢ Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₂ →' φ₁
Tactic:
apply axiomEConj₂
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
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₂} ⊢ φ₂
s2 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₂ →' φ₁
⊢ Γ ⊆ Γ ∪ {φ₂}
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.ILiff'
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 [And.intro, 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.ILiff'
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 h1 h2
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
⊢ Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Theorem: PropositionalLogic.HilbertSystem.HPM.ILiff'
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
⊢ Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Tactic:
have s1 : Γ ⊢ ((φ₁ →' φ₂) →' (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)) := by apply axiomIConj;
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
s1 : Γ ⊢ (φ₁ →' φ₂) →' (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Theorem: PropositionalLogic.HilbertSystem.HPM.ILiff'
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
s1 : Γ ⊢ (φ₁ →' φ₂) →' (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Tactic:
have s2 := MP s1 (deduction.mpr h1)
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
s1 : Γ ⊢ (φ₁ →' φ₂) →' (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s2 : Γ ⊢ (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Theorem: PropositionalLogic.HilbertSystem.HPM.ILiff'
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
s1 : Γ ⊢ (φ₁ →' φ₂) →' (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s2 : Γ ⊢ (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Tactic:
have s3 := MP s2 (deduction.mpr h2)
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
s1 : Γ ⊢ (φ₁ →' φ₂) →' (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s2 : Γ ⊢ (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s3 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Theorem: PropositionalLogic.HilbertSystem.HPM.ILiff'
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
s1 : Γ ⊢ (φ₁ →' φ₂) →' (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s2 : Γ ⊢ (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s3 : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.ILiff'
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
⊢ Γ ⊢ (φ₁ →' φ₂) →' (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Tactic:
apply axiomIConj
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.disjCommLiff
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:
apply ILiff'
Proof state after:
case a
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.disjCommLiff
Proof state before:
case a
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:
apply And.intro <;> simp [ disjComm]
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.conjCommLiff
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:
apply ILiff'
Proof state after:
case a
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.conjCommLiff
Proof state before:
case a
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:
apply And.intro <;> simp [ conjComm]
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.distDisj
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:
apply ILiff'
Proof state after:
case a
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.distDisj
Proof state before:
case a
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:
apply And.intro
Proof state after:
case a.left
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
⊢ ∅ ⊢ φ ∨' ψ ∧' χ →' (φ ∨' ψ) ∧' (φ ∨' χ)

case a.right
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.distDisj
Proof state before:
case a.left
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
⊢ ∅ ⊢ φ ∨' ψ ∧' χ →' (φ ∨' ψ) ∧' (φ ∨' χ)

case a.right
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 h1 : {φ ∨' ψ ∧' χ} ⊢ (φ ∨' ψ ∧' χ) := by simp;
  have h2 := axiomEConj₁ {φ ∨' ψ ∧' χ} (φ ∧' ψ) χ;
  have h3 := axiomEConj₂ {φ ∨' ψ ∧' χ} (φ ∧' ψ) χ;
  sorry
Proof state after:
case a.right
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.distDisj
Proof state before:
case a.right
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:
. sorry
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.distDisj
Proof state before:
case a.left
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 h1 : {φ ∨' ψ ∧' χ} ⊢ (φ ∨' ψ ∧' χ) := by simp;
Proof state after:
case a.left
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
h1 : {φ ∨' ψ ∧' χ} ⊢ φ ∨' ψ ∧' χ
⊢ ∅ ⊢ φ ∨' ψ ∧' χ →' (φ ∨' ψ) ∧' (φ ∨' χ)
Theorem: PropositionalLogic.HilbertSystem.HPM.distDisj
Proof state before:
case a.left
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
h1 : {φ ∨' ψ ∧' χ} ⊢ φ ∨' ψ ∧' χ
⊢ ∅ ⊢ φ ∨' ψ ∧' χ →' (φ ∨' ψ) ∧' (φ ∨' χ)
Tactic:
have h2 := axiomEConj₁ {φ ∨' ψ ∧' χ} (φ ∧' ψ) χ
Proof state after:
case a.left
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
h1 : {φ ∨' ψ ∧' χ} ⊢ φ ∨' ψ ∧' χ
h2 : {φ ∨' ψ ∧' χ} ⊢ φ ∧' ψ ∧' χ →' φ ∧' ψ
⊢ ∅ ⊢ φ ∨' ψ ∧' χ →' (φ ∨' ψ) ∧' (φ ∨' χ)
Theorem: PropositionalLogic.HilbertSystem.HPM.distDisj
Proof state before:
case a.left
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
h1 : {φ ∨' ψ ∧' χ} ⊢ φ ∨' ψ ∧' χ
h2 : {φ ∨' ψ ∧' χ} ⊢ φ ∧' ψ ∧' χ →' φ ∧' ψ
⊢ ∅ ⊢ φ ∨' ψ ∧' χ →' (φ ∨' ψ) ∧' (φ ∨' χ)
Tactic:
have h3 := axiomEConj₂ {φ ∨' ψ ∧' χ} (φ ∧' ψ) χ
Proof state after:
case a.left
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
h1 : {φ ∨' ψ ∧' χ} ⊢ φ ∨' ψ ∧' χ
h2 : {φ ∨' ψ ∧' χ} ⊢ φ ∧' ψ ∧' χ →' φ ∧' ψ
h3 : {φ ∨' ψ ∧' χ} ⊢ φ ∧' ψ ∧' χ →' χ
⊢ ∅ ⊢ φ ∨' ψ ∧' χ →' (φ ∨' ψ) ∧' (φ ∨' χ)
Theorem: PropositionalLogic.HilbertSystem.HPM.distDisj
Proof state before:
case a.left
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
h1 : {φ ∨' ψ ∧' χ} ⊢ φ ∨' ψ ∧' χ
h2 : {φ ∨' ψ ∧' χ} ⊢ φ ∧' ψ ∧' χ →' φ ∧' ψ
h3 : {φ ∨' ψ ∧' χ} ⊢ φ ∧' ψ ∧' χ →' χ
⊢ ∅ ⊢ φ ∨' ψ ∧' χ →' (φ ∨' ψ) ∧' (φ ∨' χ)
Tactic:
sorry
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.distDisj
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.distDisj
Proof state before:
case a.right
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:
sorry
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.distConj
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:
apply ILiff'
Proof state after:
case a
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.distConj
Proof state before:
case a
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:
apply And.intro
Proof state after:
case a.left
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
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ

case a.right
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.distConj
Proof state before:
case a.left
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
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ

case a.right
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 h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ := by simp;
  have h2 := axiomEDisj {φ ∧' ψ ∨' φ ∧' χ} φ (ψ ∨' χ) ψ;
  have h3 := axiomEDisj {φ ∧' ψ ∨' φ ∧' χ} φ (ψ ∨' χ) χ;
  sorry
Proof state after:
case a.right
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.distConj
Proof state before:
case a.right
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 h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ := by simp;
  have h5 := MP (EDisj (axiomEConj₁ _ _ _) (axiomEConj₁ _ _ _)) h1;
  sorry
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.distConj
Proof state before:
case a.left
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 h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ := by simp;
Proof state after:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ
Theorem: PropositionalLogic.HilbertSystem.HPM.distConj
Proof state before:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ
Tactic:
have h2 := axiomEDisj {φ ∧' ψ ∨' φ ∧' χ} φ (ψ ∨' χ) ψ
Proof state after:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h2 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' ψ) →' (ψ ∨' χ →' ψ) →' φ ∨' (ψ ∨' χ) →' ψ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ
Theorem: PropositionalLogic.HilbertSystem.HPM.distConj
Proof state before:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h2 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' ψ) →' (ψ ∨' χ →' ψ) →' φ ∨' (ψ ∨' χ) →' ψ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ
Tactic:
have h3 := axiomEDisj {φ ∧' ψ ∨' φ ∧' χ} φ (ψ ∨' χ) χ
Proof state after:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h2 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' ψ) →' (ψ ∨' χ →' ψ) →' φ ∨' (ψ ∨' χ) →' ψ
h3 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' χ) →' (ψ ∨' χ →' χ) →' φ ∨' (ψ ∨' χ) →' χ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ