Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2eximi | Unicode version |
Description: Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Ref | Expression |
---|---|
eximi.1 |
Ref | Expression |
---|---|
2eximi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximi.1 | . . 3 | |
2 | 1 | eximi 1580 | . 2 |
3 | 2 | eximi 1580 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 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-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: excomim 1643 cgsex2g 2748 cgsex4g 2749 vtocl2 2767 vtocl3 2768 dtruarb 4152 opelopabsb 4220 mosubopt 4651 xpmlem 5006 brabvv 5867 ssoprab2i 5910 dmaddpqlem 7297 nqpi 7298 dmaddpq 7299 dmmulpq 7300 enq0sym 7352 enq0ref 7353 enq0tr 7354 nq0nn 7362 prarloc 7423 bj-inex 13493 |
Copyright terms: Public domain | W3C validator |