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

Theorem reximi2 2804
 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 1585 . 2
3 df-rex 2703 . 2
4 df-rex 2703 . 2
52, 3, 43imtr4i 258 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359  wex 1550   wcel 1725  wrex 2698 This theorem is referenced by:  pssnn  7318  btwnz  10361  xrsupexmnf  10872  xrinfmexpnf  10873  xrsupsslem  10874  xrinfmsslem  10875  supxrun  10883  ioo0  10930  resqrex  12044  resqreu  12046  rexuzre  12144  neiptopnei  17184  filssufilg  17931  alexsubALTlem4  18069  lgsquadlem2  21127  nmobndseqi  22268  nmobndseqiOLD  22269  pjnmopi  23639  dya2iocuni  24621  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemsup  24750  comppfsc  26324  sstotbnd3  26422  aaitgo  27282  stoweidlem14  27677  stoweidlem57  27720  lsateln0  29632  pclcmpatN  30537 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566 This theorem depends on definitions:  df-bi 178  df-ex 1551  df-rex 2703
 Copyright terms: Public domain W3C validator