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

Theorem reximia 3155
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 3154 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
2 reximia.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprg 3073 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3060  df-rex 3061
This theorem is referenced by:  reximi  3157  iunpw  7176  wfrdmcl  7627  tz7.49c  7745  fisup2g  8581  fiinf2g  8613  unwdomg  8696  trcl  8819  cfsmolem  9345  1idpr  10104  qmulz  11992  zq  11995  xrsupexmnf  12337  xrinfmexpnf  12338  caubnd2  14382  caurcvg  14692  caurcvg2  14693  caucvg  14694  txlm  21731  norm1exi  28563  chrelat2i  29680  xrofsup  29982  esumcvg  30595  bnj168  31247  poimirlem30  33863  ismblfin  33874  allbutfi  40253  sge0ltfirpmpt  41262  ovolval5lem3  41508  nnsum4primes4  42353  nnsum4primesprm  42355  nnsum4primesgbe  42357  nnsum4primesle9  42359
  Copyright terms: Public domain W3C validator