Metamath Proof Explorer

Theorem bj-nnfa

Description: Nonfreeness implies the equivalent of ax-5 . See nf5r . (Contributed by BJ, 28-Jul-2023)

Ref Expression
Assertion bj-nnfa 
|- ( F// x ph -> ( ph -> A. x ph ) )

Proof

Step Hyp Ref Expression
1 df-bj-nnf 
 |-  ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) )
2 1 simprbi 
 |-  ( F// x ph -> ( ph -> A. x ph ) )