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

Theorem reximia 3229
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 3228 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
2 reximia.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprg 3139 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  wrex 3126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3130  df-rex 3131
This theorem is referenced by:  reximi  3230  iunpw  7471  wfrdmcl  7941  tz7.49c  8060  fisup2g  8910  fiinf2g  8942  unwdomg  9026  trcl  9148  cfsmolem  9670  1idpr  10429  qmulz  12330  xrsupexmnf  12677  xrinfmexpnf  12678  caubnd2  14697  caurcvg  15013  caurcvg2  15014  caucvg  15015  sgrpidmnd  17895  txlm  22232  norm1exi  29012  chrelat2i  30127  xrofsup  30479  esumcvg  31353  bnj168  32008  satfv1  32618  satfv0fvfmla0  32668  poimirlem30  34963  ismblfin  34974  dffltz  39408  allbutfi  41819  sge0ltfirpmpt  42838  ovolval5lem3  43084  2reu8i  43460  nnsum4primes4  44099  nnsum4primesprm  44101  nnsum4primesgbe  44103  nnsum4primesle9  44105
  Copyright terms: Public domain W3C validator