![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2eximi | Structured version Visualization version Unicode version |
Description: Inference adding two 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 1707 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | eximi 1707 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 |
This theorem depends on definitions: df-bi 189 df-ex 1664 |
This theorem is referenced by: 2mo 2380 2eu6 2387 cgsex2g 3081 cgsex4g 3082 vtocl2 3102 vtocl3 3103 dtru 4594 mosubopt 4699 elopaelxp 4907 xpdifid 5265 ssoprab2i 6385 hash1to3 12648 isfunc 15769 usgraop 25077 usgraedg4 25114 3v3e3cycl2 25392 frconngra 25749 bnj605 29718 bnj607 29727 bnj916 29744 bnj996 29766 bnj907 29776 bnj1128 29799 bj-dtru 31412 ac6s6f 32416 2uasbanh 36928 2uasbanhVD 37308 |
Copyright terms: Public domain | W3C validator |