Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reximi2 | Structured version Visualization version Unicode version |
Description: Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.) |
Ref | Expression |
---|---|
reximi2.1 |
Ref | Expression |
---|---|
reximi2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximi2.1 | . . 3 | |
2 | 1 | eximi 1762 | . 2 |
3 | df-rex 2918 | . 2 | |
4 | df-rex 2918 | . 2 | |
5 | 2, 3, 4 | 3imtr4i 281 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wex 1704 wcel 1990 wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-rex 2918 |
This theorem is referenced by: pssnn 8178 btwnz 11479 xrsupexmnf 12135 xrinfmexpnf 12136 xrsupsslem 12137 xrinfmsslem 12138 supxrun 12146 ioo0 12200 resqrex 13991 resqreu 13993 rexuzre 14092 neiptopnei 20936 comppfsc 21335 filssufilg 21715 alexsubALTlem4 21854 lgsquadlem2 25106 nmobndseqi 27634 nmobndseqiALT 27635 pjnmopi 29007 crefdf 29915 dya2iocuni 30345 ballotlemfc0 30554 ballotlemfcc 30555 ballotlemsup 30566 poimirlem32 33441 sstotbnd3 33575 lsateln0 34282 pclcmpatN 35187 aaitgo 37732 stoweidlem14 40231 stoweidlem57 40274 elaa2 40451 |
Copyright terms: Public domain | W3C validator |