![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2exbii | Unicode version |
Description: Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Ref | Expression |
---|---|
exbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2exbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbii.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | exbii 1616 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | exbii 1616 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3exbii 1618 19.42vvvv 1925 3exdistr 1927 cbvex4v 1942 ee4anv 1946 ee8anv 1947 sbel2x 2010 2eu4 2131 rexcomf 2652 reean 2659 ceqsex3v 2794 ceqsex4v 2795 ceqsex8v 2797 copsexg 4262 opelopabsbALT 4277 opabm 4298 uniuni 4469 rabxp 4681 elxp3 4698 elvv 4706 elvvv 4707 rexiunxp 4787 elcnv2 4823 cnvuni 4831 coass 5165 fununi 5303 dfmpt3 5357 dfoprab2 5943 dmoprab 5977 rnoprab 5979 mpomptx 5987 resoprab 5992 ovi3 6033 ov6g 6034 oprabex3 6154 xpassen 6856 enq0enq 7460 enq0sym 7461 enq0tr 7463 ltresr 7868 axaddf 7897 axmulf 7898 |
Copyright terms: Public domain | W3C validator |