Theorem: HTPI.two_imp (HTPILib/IntroLean.lean)

State before:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
⊢ R → ¬P
Tactic:
contrapos
State after:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
⊢ P → ¬R

State before:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
⊢ P → ¬R
Tactic:
assume h3 : P
State after:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
h3 : P
⊢ ¬R

State before:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
h3 : P
⊢ ¬R
Tactic:
have h4 : Q := h1 h3
State after:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
h3 : P
h4 : Q
⊢ ¬R

State before:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
h3 : P
h4 : Q
⊢ ¬R
Tactic:
show ¬R from h2 h4
State after:
no goals