Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mp (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:
simp [deduction]
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
⊢ (Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)) → (Γ ∪ {φ₁} ⊢ φ₂)

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:
have s1 : Γ ∪ {φ₁} ⊢ φ₁ := by simp;
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 : Γ ∪ {φ₁} ⊢ φ₁
⊢ Γ ∪ {φ₁} ⊢ φ₂

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₁;
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 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₁ →' φ₂
⊢ Γ ∪ {φ₁} ⊢ φ₂

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
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 : Γ ∪ {φ₁} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₁} ⊢ φ₂

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
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 : Γ ∪ {φ₁} ⊢ φ₁ →' φ₂
⊢ Γ ∪ {φ₁} ⊢ φ₂

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
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 : Γ ∪ {φ₁} ⊢ φ₂
⊢ Γ ∪ {φ₁} ⊢ φ₂

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
State after:
no goals

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
State after:
no goals

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₁
State after:
no goals

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
State after:
no goals