Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > excom | GIF version |
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
excom | ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | excomim 1643 | . 2 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑) | |
2 | excomim 1643 | . 2 ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑) | |
3 | 1, 2 | impbii 125 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∃wex 1472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: excom13 1669 exrot3 1670 ee4anv 1914 sbexyz 1983 2exsb 1989 2euex 2093 2exeu 2098 2eu4 2099 rexcomf 2619 gencbvex 2758 euxfr2dc 2897 euind 2899 sbccomlem 3011 opelopabsbALT 4219 uniuni 4411 elvvv 4649 elco 4752 dmuni 4796 dm0rn0 4803 dmmrnm 4805 dmcosseq 4857 elres 4902 rnco 5092 coass 5104 oprabid 5853 dfoprab2 5868 opabex3d 6069 opabex3 6070 cnvoprab 6181 domen 6696 xpassen 6775 prarloc 7423 fisumcom2 11335 fprodcom2fi 11523 |
Copyright terms: Public domain | W3C validator |