Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Nonfreeness
bj-nnfth
Next ⟩
bj-nnfnth
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-nnfth
Description:
A variable is nonfree in a theorem, inference form.
(Contributed by
BJ
, 28-Jul-2023)
Ref
Expression
Hypothesis
bj-nnfth.1
⊢
φ
Assertion
bj-nnfth
⊢
Ⅎ'
x
φ
Proof
Step
Hyp
Ref
Expression
1
bj-nnfth.1
⊢
φ
2
bj-nnftht
⊢
φ
∧
∀
x
φ
→
Ⅎ'
x
φ
3
1
2
bj-mpgs
⊢
Ⅎ'
x
φ