Metamath Proof Explorer

Theorem bj-nnfalt

Description: See nfal and bj-nfalt . (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 df-bj-nnf 
 |-  ( F// y ph <-> ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) )
2 1 albii 
 |-  ( A. x F// y ph <-> A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) )
3 simpl 
 |-  ( ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> ( E. y ph -> ph ) )
4 3 alimi 
 |-  ( A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> A. x ( E. y ph -> ph ) )
5 bj-nnflemea 
 |-  ( A. x ( E. y ph -> ph ) -> ( E. y A. x ph -> A. x ph ) )
6 4 5 syl 
 |-  ( A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> ( E. y A. x ph -> A. x ph ) )
7 2 6 sylbi 
 |-  ( A. x F// y ph -> ( E. y A. x ph -> A. x ph ) )
8 simpr 
 |-  ( ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> ( ph -> A. y ph ) )
9 8 alimi 
 |-  ( A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> A. x ( ph -> A. y ph ) )
10 bj-nnflemaa 
 |-  ( A. x ( ph -> A. y ph ) -> ( A. x ph -> A. y A. x ph ) )
11 9 10 syl 
 |-  ( A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> ( A. x ph -> A. y A. x ph ) )
12 2 11 sylbi 
 |-  ( A. x F// y ph -> ( A. x ph -> A. y A. x ph ) )
13 df-bj-nnf 
 |-  ( F// y A. x ph <-> ( ( E. y A. x ph -> A. x ph ) /\ ( A. x ph -> A. y A. x ph ) ) )
14 7 12 13 sylanbrc 
 |-  ( A. x F// y ph -> F// y A. x ph )