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

Theorem reximia 2987
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 2986 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
2 reximia.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprg 2905 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1975  wrex 2892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2896  df-rex 2897
This theorem is referenced by:  reximi  2989  iunpw  6843  wfrdmcl  7283  tz7.49c  7401  fisup2g  8230  fiinf2g  8262  unwdomg  8345  trcl  8460  cfsmolem  8948  1idpr  9703  qmulz  11619  zq  11622  xrsupexmnf  11959  xrinfmexpnf  11960  caubnd2  13887  caurcvg  14197  caurcvg2  14198  caucvg  14199  txlm  21199  norm1exi  27293  chrelat2i  28410  xrofsup  28725  esumcvg  29277  bnj168  29854  poimirlem30  32408  ismblfin  32419  allbutfi  38357  sge0ltfirpmpt  39101  ovolval5lem3  39344  nnsum4primes4  40006  nnsum4primesprm  40008  nnsum4primesgbe  40010  nnsum4primesle9  40012
  Copyright terms: Public domain W3C validator