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

Theorem reximia 2992
 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 2991 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
2 reximia.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprg 2910 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902 This theorem is referenced by:  reximi  2994  iunpw  6870  wfrdmcl  7310  tz7.49c  7428  fisup2g  8257  fiinf2g  8289  unwdomg  8372  trcl  8487  cfsmolem  8975  1idpr  9730  qmulz  11667  zq  11670  xrsupexmnf  12007  xrinfmexpnf  12008  caubnd2  13945  caurcvg  14255  caurcvg2  14256  caucvg  14257  txlm  21261  norm1exi  27491  chrelat2i  28608  xrofsup  28923  esumcvg  29475  bnj168  30052  poimirlem30  32609  ismblfin  32620  allbutfi  38557  sge0ltfirpmpt  39301  ovolval5lem3  39544  nnsum4primes4  40205  nnsum4primesprm  40207  nnsum4primesgbe  40209  nnsum4primesle9  40211
 Copyright terms: Public domain W3C validator