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

Theorem reximia 2923
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)
Hypothesis
Ref Expression
reximia.1
Assertion
Ref Expression
reximia

Proof of Theorem reximia
StepHypRef Expression
1 rexim 2922 . 2
2 reximia.1 . 2
31, 2mprg 2820 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  reximi  2925  iunpw  6614  tz7.49c  7130  fisup2g  7947  unwdomg  8031  trcl  8180  cfsmolem  8671  1idpr  9428  qmulz  11214  zq  11217  xrsupexmnf  11525  xrinfmexpnf  11526  caubnd2  13190  caurcvg  13499  caurcvg2  13500  caucvg  13501  txlm  20149  norm1exi  26168  chrelat2i  27284  xrofsup  27582  esumcvg  28092  wfrlem9  29351  ismblfin  30055  bnj168  33785
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-an 371  df-ex 1613  df-ral 2812  df-rex 2813
  Copyright terms: Public domain W3C validator