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 1579 | . 2 |
3 | 2 | eximi 1579 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1468 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: excomim 1641 cgsex2g 2722 cgsex4g 2723 vtocl2 2741 vtocl3 2742 dtruarb 4115 opelopabsb 4182 mosubopt 4604 xpmlem 4959 brabvv 5817 ssoprab2i 5860 dmaddpqlem 7185 nqpi 7186 dmaddpq 7187 dmmulpq 7188 enq0sym 7240 enq0ref 7241 enq0tr 7242 nq0nn 7250 prarloc 7311 bj-inex 13105 |
Copyright terms: Public domain | W3C validator |