Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Adding ax-6
bj-modald
Next ⟩
bj-denot
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-modald
Description:
A short form of the axiom D of modal logic.
(Contributed by
BJ
, 4-Apr-2021)
Ref
Expression
Assertion
bj-modald
⊢
∀
x
¬
φ
→
¬
∀
x
φ
Proof
Step
Hyp
Ref
Expression
1
19.2
⊢
∀
x
φ
→
∃
x
φ
2
df-ex
⊢
∃
x
φ
↔
¬
∀
x
¬
φ
3
1
2
sylib
⊢
∀
x
φ
→
¬
∀
x
¬
φ
4
3
con2i
⊢
∀
x
¬
φ
→
¬
∀
x
φ