![]() |
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 1567 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | exbii 1567 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-4 1470 ax-ial 1497 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3exbii 1569 19.42vvvv 1865 3exdistr 1867 cbvex4v 1880 ee4anv 1884 ee8anv 1885 sbel2x 1949 2eu4 2068 rexcomf 2567 reean 2573 ceqsex3v 2699 ceqsex4v 2700 ceqsex8v 2702 copsexg 4126 opelopabsbALT 4141 opabm 4162 uniuni 4332 rabxp 4536 elxp3 4553 elvv 4561 elvvv 4562 rexiunxp 4641 elcnv2 4677 cnvuni 4685 coass 5015 fununi 5149 dfmpt3 5203 dfoprab2 5772 dmoprab 5806 rnoprab 5808 mpomptx 5816 resoprab 5821 ovi3 5861 ov6g 5862 oprabex3 5981 xpassen 6677 enq0enq 7187 enq0sym 7188 enq0tr 7190 ltresr 7574 axaddf 7603 axmulf 7604 |
Copyright terms: Public domain | W3C validator |