![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2exbii | Structured version Visualization version Unicode version |
Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Ref | Expression |
---|---|
2exbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2exbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2exbii.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | exbii 1718 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | exbii 1718 |
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: 3exbii 1720 3exdistr 1839 eeeanv 2079 ee4anv 2080 cbvex4v 2126 2sb5rf 2280 sbel2x 2288 2exsb 2298 2mo2 2379 rexcomf 2950 reean 2957 ceqsex3v 3088 ceqsex4v 3089 ceqsex8v 3091 vtocl3 3103 copsexg 4687 opelopabsbALT 4710 opabn0 4732 rabxp 4871 elxp3 4885 elvv 4893 elvvv 4894 copsex2gb 4945 elcnv2 5012 cnvuni 5021 xpdifid 5265 coass 5354 fununi 5649 dfmpt3 5698 tpres 6117 dfoprab2 6337 dmoprab 6377 rnoprab 6379 mpt2mptx 6387 resoprab 6392 elrnmpt2res 6410 ov3 6433 ov6g 6434 uniuni 6600 oprabex3 6782 wfrlem4 7039 oeeu 7304 xpassen 7666 zorn2lem6 8931 ltresr 9564 axaddf 9569 axmulf 9570 hashfun 12609 hash2prb 12633 5oalem7 27313 mpt2mptxf 28280 eulerpartlemgvv 29209 bnj600 29730 bnj916 29744 bnj983 29762 bnj986 29765 bnj996 29766 bnj1021 29775 elima4 30421 brtxp2 30648 brpprod3a 30653 brpprod3b 30654 elfuns 30682 brcart 30699 brimg 30704 brapply 30705 brsuccf 30708 brrestrict 30716 dfrdg4 30718 ellines 30919 bj-cbvex4vv 31344 itg2addnclem3 31995 dalem20 33258 dvhopellsm 34685 diblsmopel 34739 pm11.52 36736 2exanali 36737 pm11.6 36742 pm11.7 36746 opelopab4 36918 stoweidlem35 37896 mpt2mptx2 40169 |
Copyright terms: Public domain | W3C validator |