Metamath Proof Explorer

Table of Contents - 1.5.2. Axiom scheme ax-11 (Quantifier Commutation)

1. ax-11
2. alcoms
3. alcom
4. alrot3
5. alrot4
6. sbal
7. sbalv
8. sbcom2
9. excom
10. excomim
11. excom13
12. exrot3
13. exrot4
14. hbal
15. hbald
16. hbsbw
17. nfa2