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

Theorem reximia 3038
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 3037 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
2 reximia.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprg 2955 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  reximi  3040  iunpw  7020  wfrdmcl  7468  tz7.49c  7586  fisup2g  8415  fiinf2g  8447  unwdomg  8530  trcl  8642  cfsmolem  9130  1idpr  9889  qmulz  11829  zq  11832  xrsupexmnf  12173  xrinfmexpnf  12174  caubnd2  14141  caurcvg  14451  caurcvg2  14452  caucvg  14453  txlm  21499  norm1exi  28235  chrelat2i  29352  xrofsup  29661  esumcvg  30276  bnj168  30924  poimirlem30  33569  ismblfin  33580  allbutfi  39929  sge0ltfirpmpt  40943  ovolval5lem3  41189  nnsum4primes4  42002  nnsum4primesprm  42004  nnsum4primesgbe  42006  nnsum4primesle9  42008
  Copyright terms: Public domain W3C validator