| 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 2044 when it allows to avoid dependence on ax-11 2157. (Contributed by NM, 30-Jun-1993.) |
| Ref | Expression |
|---|---|
| alcom | ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-11 2157 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | |
| 2 | ax-11 2157 | . 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
| 3 | 1, 2 | impbii 209 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∀wal 1538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-11 2157 |
| This theorem depends on definitions: df-bi 207 |
| This theorem is referenced by: alrot3 2160 excom 2162 sbal 2169 sbcom2 2173 nfa2 2176 aaan 2333 sb8v 2355 sb8f 2356 sbnf2 2361 sbal1 2533 sbal2 2534 2mo2 2647 ralcom4 3286 ralcom4OLD 3287 ralcom 3289 nfra2wOLD 3300 ralcomf 3302 moelOLD 3405 sbccomlem 3869 unissbOLD 4940 dfiin2g 5032 dftr5OLD 5264 cotrgOLD 6128 cotrgOLDOLD 6129 cnvsymOLD 6133 cnvsymOLDOLD 6134 dffun2OLD 6572 dffun2OLDOLD 6573 fun11 6640 aceq1 10157 isch2 31242 dfon2lem8 35791 bj-hbaeb 36820 wl-sb9v 37550 wl-sbcom2d 37562 wl-sbalnae 37563 wl-2spsbbi 37566 cocossss 38437 cossssid3 38470 trcoss2 38485 dford4 43041 unielss 43230 elmapintrab 43589 undmrnresiss 43617 cnvssco 43619 elintima 43666 relexp0eq 43714 dfhe3 43788 dffrege115 43991 hbexg 44576 hbexgVD 44926 dfich2 47445 ichcom 47446 |
| Copyright terms: Public domain | W3C validator |