![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2rexbii | Structured version Visualization version Unicode version |
Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.) |
Ref | Expression |
---|---|
rexbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2rexbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexbii.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rexbii 2888 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rexbii 2888 |
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 1668 ax-4 1681 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1663 df-rex 2742 |
This theorem is referenced by: ralnex2 2892 ralnex3 2893 3reeanv 2958 addcompr 9443 mulcompr 9445 4fvwrd4 11906 ntrivcvgmul 13951 prodmo 13983 pythagtriplem2 14760 pythagtrip 14777 isnsgrp 16524 efgrelexlemb 17393 ordthaus 20393 regr1lem2 20748 fmucndlem 21299 dfcgra2 24864 axpasch 24964 axeuclid 24986 axcontlem4 24990 frgrawopreglem5 25769 xrofsup 28346 poseq 30484 altopelaltxp 30736 brsegle 30868 mzpcompact2lem 35587 sbc4rex 35626 7rexfrabdioph 35637 expdiophlem1 35870 fourierdlem42 38006 fourierdlem42OLD 38007 usgr2edg1 39278 ldepslinc 40289 |
Copyright terms: Public domain | W3C validator |