![]() |
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. (Contributed by NM, 30-Jun-1993.) |
Ref | Expression |
---|---|
alcom | ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-11 2093 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | |
2 | ax-11 2093 | . 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
3 | 1, 2 | impbii 201 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∀wal 1505 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-11 2093 |
This theorem depends on definitions: df-bi 199 |
This theorem is referenced by: alrot3 2096 excom 2098 nfa2 2105 sbnf2 2291 sbcom2 2410 sbcom2OLD 2411 sbal1 2495 sbal2 2496 sbal2OLD 2497 sbal2OLDOLD 2498 sbal 2499 nexmoOLD 2549 2mo2 2679 ralcom4 3183 ralcom 3296 ralcomf 3299 unissb 4743 dfiin2g 4827 dftr5 5033 cotrg 5811 cnvsym 5814 dffun2 6198 fun11 6261 aceq1 9337 isch2 28779 moel 30034 dfon2lem8 32552 bj-hbaeb 33630 wl-sbcom2d 34235 wl-sbalnae 34236 wl-2spsbbi 34239 wl-dfralflem 34276 cocossss 35123 cossssid3 35151 trcoss2 35166 dford4 39019 elmapintrab 39295 undmrnresiss 39323 cnvssco 39325 elintima 39358 relexp0eq 39406 dfhe3 39481 dffrege115 39684 hbexg 40306 hbexgVD 40656 dfich2 42981 dfich2ai 42982 ichcom 42985 |
Copyright terms: Public domain | W3C validator |