Metamath Proof Explorer


Theorem nf5di

Description: Since the converse holds by a1i , this inference shows that we can represent a not-free hypothesis with either F/ x ph (inference form) or ( ph -> F/ x ph ) (deduction form). (Contributed by NM, 17-Aug-2018) (Proof shortened by Wolf Lammen, 10-Jul-2019)

Ref Expression
Hypothesis nf5di.1 φ x φ
Assertion nf5di x φ

Proof

Step Hyp Ref Expression
1 nf5di.1 φ x φ
2 1 nf5rd φ φ x φ
3 2 pm2.43i φ x φ
4 3 nf5i x φ