Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical negation
conax1
Next ⟩
conax1k
Metamath Proof Explorer
Ascii
Structured
Theorem
conax1
Description:
Contrapositive of
ax-1
.
(Contributed by
BJ
, 28-Oct-2023)
Ref
Expression
Assertion
conax1
⊢
( ¬ (
𝜑
→
𝜓
) → ¬
𝜓
)
Proof
Step
Hyp
Ref
Expression
1
ax-1
⊢
(
𝜓
→ (
𝜑
→
𝜓
) )
2
1
con3i
⊢
( ¬ (
𝜑
→
𝜓
) → ¬
𝜓
)