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 2151 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | |
2 | ax-11 2151 | . 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
3 | 1, 2 | impbii 210 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-11 2151 |
This theorem depends on definitions: df-bi 208 |
This theorem is referenced by: alrot3 2154 sbal 2156 sbcom2 2158 excom 2159 nfa2 2166 sbnf2 2368 sbal1 2565 sbal2 2566 sbal2OLD 2567 2mo2 2725 ralcom4 3232 ralcom 3351 ralcomf 3354 unissb 4861 dfiin2g 4948 dftr5 5166 cotrg 5964 cnvsym 5967 dffun2 6358 fun11 6421 aceq1 9531 isch2 28927 moel 30179 dfon2lem8 32932 bj-hbaeb 34039 wl-sbcom2d 34678 wl-sbalnae 34679 wl-2spsbbi 34682 wl-dfralflem 34719 cocossss 35561 cossssid3 35589 trcoss2 35604 dford4 39504 elmapintrab 39814 undmrnresiss 39842 cnvssco 39844 elintima 39876 relexp0eq 39924 dfhe3 39999 dffrege115 40202 hbexg 40767 hbexgVD 41117 dfich2 43490 dfich2ai 43491 ichcom 43494 |
Copyright terms: Public domain | W3C validator |