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 2021 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | |
2 | ax-11 2021 | . 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
3 | 1, 2 | impbii 198 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-11 2021 |
This theorem depends on definitions: df-bi 196 |
This theorem is referenced by: alrot3 2025 nfa2 2027 excom 2029 sbnf2 2427 sbcom2 2433 sbal1 2448 sbal2 2449 2mo2 2538 ralcomf 3077 unissb 4405 dfiin2g 4489 dftr5 4683 cotrg 5426 cnvsym 5429 dffun2 5814 fun11 5877 aceq1 8823 isch2 27464 moel 28707 dfon2lem8 30939 bj-ssb1 31822 bj-hbaeb 31994 bj-ralcom4 32062 wl-sbcom2d 32523 wl-sbalnae 32524 dford4 36614 elmapintrab 36901 undmrnresiss 36929 cnvssco 36931 elintima 36964 relexp0eq 37012 dfhe3 37089 dffrege115 37292 hbexg 37793 hbexgVD 38164 |
Copyright terms: Public domain | W3C validator |