Description: Weak version of alcom and biconditional form of alcomiw . Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 28-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | alcomw.1 | |- ( x = w -> ( ph <-> ps ) ) |
|
alcomw.2 | |- ( y = z -> ( ph <-> ch ) ) |
||
Assertion | alcomw | |- ( A. x A. y ph <-> A. y A. x ph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alcomw.1 | |- ( x = w -> ( ph <-> ps ) ) |
|
2 | alcomw.2 | |- ( y = z -> ( ph <-> ch ) ) |
|
3 | 2 | alcomiw | |- ( A. x A. y ph -> A. y A. x ph ) |
4 | 1 | alcomiw | |- ( A. y A. x ph -> A. x A. y ph ) |
5 | 3 4 | impbii | |- ( A. x A. y ph <-> A. y A. x ph ) |