![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > alcom | GIF version |
Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
alcom | ⊢ (∀x∀yφ ↔ ∀y∀xφ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-7 1334 | . 2 ⊢ (∀x∀yφ → ∀y∀xφ) | |
2 | ax-7 1334 | . 2 ⊢ (∀y∀xφ → ∀x∀yφ) | |
3 | 1, 2 | impbii 117 | 1 ⊢ (∀x∀yφ ↔ ∀y∀xφ) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∀wal 1240 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 100 ax-ia3 101 ax-7 1334 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: alrot3 1371 alrot4 1372 nfalt 1467 nfexd 1641 sbnf2 1854 sbcom2v 1858 sbalyz 1872 sbal1yz 1874 sbal2 1895 2eu4 1990 ralcomf 2465 gencbval 2596 unissb 3601 dfiin2g 3681 dftr5 3848 cotr 4649 cnvsym 4651 dffun2 4855 funcnveq 4905 fun11 4909 |
Copyright terms: Public domain | W3C validator |