MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximi2 Unicode version

Theorem reximi2 2924
Description: Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)
Hypothesis
Ref Expression
reximi2.1
Assertion
Ref Expression
reximi2

Proof of Theorem reximi2
StepHypRef Expression
1 reximi2.1 . . 3
21eximi 1656 . 2
3 df-rex 2813 . 2
4 df-rex 2813 . 2
52, 3, 43imtr4i 266 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  E.wex 1612  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  pssnn  7758  btwnz  10991  xrsupexmnf  11525  xrinfmexpnf  11526  xrsupsslem  11527  xrinfmsslem  11528  supxrun  11536  ioo0  11583  resqrex  13084  resqreu  13086  rexuzre  13185  neiptopnei  19633  comppfsc  20033  filssufilg  20412  alexsubALTlem4  20550  lgsquadlem2  23630  nmobndseqi  25694  nmobndseqiOLD  25695  pjnmopi  27067  crefdf  27851  dya2iocuni  28254  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemsup  28443  sstotbnd3  30272  aaitgo  31111  stoweidlem14  31796  stoweidlem57  31839  elaa2  32017  lsateln0  34720  pclcmpatN  35625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-rex 2813
  Copyright terms: Public domain W3C validator