![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alcom | Structured version Visualization version GIF version |
Description: Theorem 19.5 of [Margaris] p. 89. Use its weak version alcomw 2039 when it allows to avoid dependence on ax-11 2146. (Contributed by NM, 30-Jun-1993.) |
Ref | Expression |
---|---|
alcom | ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-11 2146 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | |
2 | ax-11 2146 | . 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
3 | 1, 2 | impbii 208 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∀wal 1531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-11 2146 |
This theorem depends on definitions: df-bi 206 |
This theorem is referenced by: alrot3 2149 excom 2151 sbal 2158 sbcom2 2162 nfa2 2165 aaan 2321 sb8v 2342 sb8f 2343 sbnf2 2348 sbal1 2521 sbal2 2522 2mo2 2635 ralcom4 3273 ralcom4OLD 3274 ralcom 3276 nfra2wOLD 3287 ralcomf 3289 moelOLD 3388 unissbOLD 4944 dfiin2g 5036 dftr5OLD 5271 cotrgOLD 6115 cotrgOLDOLD 6116 cnvsymOLD 6120 cnvsymOLDOLD 6121 dffun2OLD 6560 dffun2OLDOLD 6561 fun11 6628 aceq1 10142 isch2 31105 dfon2lem8 35517 bj-hbaeb 36427 wl-sb9v 37147 wl-sbcom2d 37159 wl-sbalnae 37160 wl-2spsbbi 37163 cocossss 38038 cossssid3 38071 trcoss2 38086 dford4 42592 unielss 42788 elmapintrab 43148 undmrnresiss 43176 cnvssco 43178 elintima 43225 relexp0eq 43273 dfhe3 43347 dffrege115 43550 hbexg 44137 hbexgVD 44487 dfich2 46935 ichcom 46936 |
Copyright terms: Public domain | W3C validator |