Step |
Hyp |
Ref |
Expression |
1 |
|
bj-hbyfrbi |
|- ( ( ( ph <-> ps ) /\ A. x ( ph <-> ps ) ) -> ( ( E. x ph -> ph ) <-> ( E. x ps -> ps ) ) ) |
2 |
|
bj-hbxfrbi |
|- ( ( ( ph <-> ps ) /\ A. x ( ph <-> ps ) ) -> ( ( ph -> A. x ph ) <-> ( ps -> A. x ps ) ) ) |
3 |
1 2
|
anbi12d |
|- ( ( ( ph <-> ps ) /\ A. x ( ph <-> ps ) ) -> ( ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) <-> ( ( E. x ps -> ps ) /\ ( ps -> A. x ps ) ) ) ) |
4 |
|
df-bj-nnf |
|- ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) ) |
5 |
|
df-bj-nnf |
|- ( F// x ps <-> ( ( E. x ps -> ps ) /\ ( ps -> A. x ps ) ) ) |
6 |
3 4 5
|
3bitr4g |
|- ( ( ( ph <-> ps ) /\ A. x ( ph <-> ps ) ) -> ( F// x ph <-> F// x ps ) ) |