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

Theorem reximia 3005
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 3004 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
2 reximia.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprg 2922 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2913  df-rex 2914
This theorem is referenced by:  reximi  3007  iunpw  6940  wfrdmcl  7383  tz7.49c  7501  fisup2g  8334  fiinf2g  8366  unwdomg  8449  trcl  8564  cfsmolem  9052  1idpr  9811  qmulz  11751  zq  11754  xrsupexmnf  12094  xrinfmexpnf  12095  caubnd2  14047  caurcvg  14357  caurcvg2  14358  caucvg  14359  txlm  21391  norm1exi  27995  chrelat2i  29112  xrofsup  29418  esumcvg  29971  bnj168  30559  poimirlem30  33110  ismblfin  33121  allbutfi  39115  sge0ltfirpmpt  39962  ovolval5lem3  40205  nnsum4primes4  40996  nnsum4primesprm  40998  nnsum4primesgbe  41000  nnsum4primesle9  41002
  Copyright terms: Public domain W3C validator