Theorem: PropositionalLogic.HilbertSystem.HPM.ILiff' (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 [And.intro, 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 h1 h2
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 : Γ ∪ {φ₂} ⊢ φ₁
⊢ Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)

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

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

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

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
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
h1 : Γ ∪ {φ₁} ⊢ φ₂
h2 : Γ ∪ {φ₂} ⊢ φ₁
⊢ Γ ⊢ (φ₁ →' φ₂) →' (φ₂ →' φ₁) →' (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
Tactic:
apply axiomIConj
State after:
no goals