Step |
Hyp |
Ref |
Expression |
1 |
|
wl-equsal1i.1 |
|- ( F/ x ph \/ F/ y ph ) |
2 |
|
wl-equsal1i.2 |
|- ( x = y -> ph ) |
3 |
2
|
gen2 |
|- A. x A. y ( x = y -> ph ) |
4 |
|
sp |
|- ( A. y A. x ( x = y -> ph ) -> A. x ( x = y -> ph ) ) |
5 |
4
|
alcoms |
|- ( A. x A. y ( x = y -> ph ) -> A. x ( x = y -> ph ) ) |
6 |
|
wl-equsal1t |
|- ( F/ x ph -> ( A. x ( x = y -> ph ) <-> ph ) ) |
7 |
5 6
|
syl5ib |
|- ( F/ x ph -> ( A. x A. y ( x = y -> ph ) -> ph ) ) |
8 |
|
wl-equsalcom |
|- ( A. y ( y = x -> ph ) <-> A. y ( x = y -> ph ) ) |
9 |
|
wl-equsal1t |
|- ( F/ y ph -> ( A. y ( y = x -> ph ) <-> ph ) ) |
10 |
9
|
biimpd |
|- ( F/ y ph -> ( A. y ( y = x -> ph ) -> ph ) ) |
11 |
8 10
|
syl5bir |
|- ( F/ y ph -> ( A. y ( x = y -> ph ) -> ph ) ) |
12 |
11
|
spsd |
|- ( F/ y ph -> ( A. x A. y ( x = y -> ph ) -> ph ) ) |
13 |
7 12
|
jaoi |
|- ( ( F/ x ph \/ F/ y ph ) -> ( A. x A. y ( x = y -> ph ) -> ph ) ) |
14 |
1 3 13
|
mp2 |
|- ph |