Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for ML
Miscellaneous
exlimim
Next ⟩
exlimimd
Metamath Proof Explorer
Ascii
Unicode
Theorem
exlimim
Description:
Closed form of
exlimimd
.
(Contributed by
ML
, 17-Jul-2020)
Ref
Expression
Assertion
exlimim
⊢
∃
x
φ
∧
∀
x
φ
→
ψ
→
ψ
Proof
Step
Hyp
Ref
Expression
1
nfa1
⊢
Ⅎ
x
∀
x
φ
→
ψ
2
nfv
⊢
Ⅎ
x
ψ
3
sp
⊢
∀
x
φ
→
ψ
→
φ
→
ψ
4
1
2
3
exlimd
⊢
∀
x
φ
→
ψ
→
∃
x
φ
→
ψ
5
4
impcom
⊢
∃
x
φ
∧
∀
x
φ
→
ψ
→
ψ