Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Adding ax-6
bj-spnfw
Next ⟩
bj-cbvexiw
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-spnfw
Description:
Theorem close to a closed form of
spnfw
.
(Contributed by
BJ
, 12-May-2019)
Ref
Expression
Assertion
bj-spnfw
⊢
∃
x
φ
→
ψ
→
∀
x
φ
→
ψ
Proof
Step
Hyp
Ref
Expression
1
19.2
⊢
∀
x
φ
→
∃
x
φ
2
1
imim1i
⊢
∃
x
φ
→
ψ
→
∀
x
φ
→
ψ