Theorem: LO.System.andImplyIffImplyImply'! (Logic/Logic/HilbertStyle/Basic.lean)

State before:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r ↔ 𝓢 ⊢! p ⟶ q ⟶ r
Tactic:
apply Iff.intro
State after:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r → 𝓢 ⊢! p ⟶ q ⟶ r

case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r

State before:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r → 𝓢 ⊢! p ⟶ q ⟶ r

case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r
Tactic:
. intro ⟨h⟩; exact ⟨andImplyIffImplyImply'.mp h⟩
State after:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r

State before:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r
Tactic:
. intro ⟨h⟩; exact ⟨andImplyIffImplyImply'.mpr h⟩
State after:
no goals

State before:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r → 𝓢 ⊢! p ⟶ q ⟶ r
Tactic:
intro ⟨h⟩
State after:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
h : 𝓢 ⊢ p ⋏ q ⟶ r
⊢ 𝓢 ⊢! p ⟶ q ⟶ r

State before:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
h : 𝓢 ⊢ p ⋏ q ⟶ r
⊢ 𝓢 ⊢! p ⟶ q ⟶ r
Tactic:
exact ⟨andImplyIffImplyImply'.mp h⟩
State after:
no goals

State before:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r
Tactic:
intro ⟨h⟩
State after:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
h : 𝓢 ⊢ p ⟶ q ⟶ r
⊢ 𝓢 ⊢! p ⋏ q ⟶ r

State before:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
h : 𝓢 ⊢ p ⟶ q ⟶ r
⊢ 𝓢 ⊢! p ⋏ q ⟶ r
Tactic:
exact ⟨andImplyIffImplyImply'.mpr h⟩
State after:
no goals