Metamath Proof Explorer

Theorem bj-nnfea

Description: Nonfreeness implies the equivalent of ax5ea . (Contributed by BJ, 28-Jul-2023)

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

Proof

Step Hyp Ref Expression
1 bj-nnfe 
 |-  ( F// x ph -> ( E. x ph -> ph ) )
2 bj-nnfa 
 |-  ( F// x ph -> ( ph -> A. x ph ) )
3 1 2 syld 
 |-  ( F// x ph -> ( E. x ph -> A. x ph ) )