Theorem reximi 3245

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)

Hypothesis

Ref	Expression
reximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
reximi	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reximi

Step	Hyp	Ref	Expression
1		reximi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	reximia 3244	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  r19.29r  3257  2r19.29  3336  r19.29d2r  3337  r19.29vva  3338  r19.35  3343  r19.40  3348  2reu2rex  3434  reu3  3720  2reu5  3751  reuan  3882  ssiun  4972  iinss  4982  elsnxp  6144  elunirn  7012  iiner  8371  erovlem  8395  xpf1o  8681  unbnn2  8777  scott0  9317  dfac2b  9558  cflm  9674  alephsing  9700  numthcor  9918  zorng  9928  zornn0g  9929  ttukeyg  9941  uniimadom  9968  axgroth3  10255  qextlt  12599  qextle  12600  mptnn0fsuppd  13369  hashgt23el  13788  hash2sspr  13849  cshword  14155  rexanre  14708  climi2  14870  climi0  14871  rlimres  14917  lo1res  14918  caurcvgr  15032  caurcvg2  15036  caucvgb  15038  prodmolem2  15291  prodmo  15292  vdwnnlem1  16333  cshwsiun  16435  isnmnd  17917  efgrelexlemb  18878  nn0gsumfz0  19107  ablsimpgfind  19234  pmatcollpw2lem  21387  eltg2b  21569  neiptopuni  21740  neiptopnei  21742  ordtbas2  21801  lmcvg  21872  cnprest  21899  lmcnp  21914  nrmsep2  21966  bwth  22020  1stcfb  22055  islly2  22094  llycmpkgen  22162  txbas  22177  tx1stc  22260  cnextcn  22677  tmdcn2  22699  utoptop  22845  ucnima  22892  cfiluweak  22906  metrest  23136  metust  23170  cfilucfil  23171  metustbl  23178  xrhmeo  23552  cmetcaulem  23893  iundisj  24151  limcresi  24485  elply2  24788  aalioulem2  24924  ulmf  24972  lgamucov2  25618  2sqlem7  26002  2sqreultblem  26026  2sqreunnltblem  26029  pntrsumbnd  26144  istrkg2ld  26248  tgisline  26415  umgr2edgneu  26998  umgr3v3e3cycl  27965  eucrctshift  28024  1to3vfriendship  28062  2pthfrgrrn  28063  grpoidval  28292  grporcan  28297  grpoinveu  28298  iunrnmptss  30319  iundisjf  30341  xlt2addrd  30484  xrofsup  30494  iundisjfi  30521  rhmdvdsr  30893  tpr2rico  31157  esumc  31312  esumfsup  31331  esumpcvgval  31339  hasheuni  31346  esumiun  31355  voliune  31490  volfiniune  31491  dya2icoseg2  31538  dya2iocnei  31542  dya2iocuni  31543  omssubaddlem  31559  omssubadd  31560  afsval  31944  bnj31  31991  bnj1239  32079  bnj900  32203  bnj906  32204  bnj1398  32308  bnj1498  32335  satfvsuclem1  32608  satfv1  32612  satfvsucsuc  32614  nosupno  33205  nosupfv  33208  colinearex  33523  segcon2  33568  opnrebl2  33671  nlpfvineqsn  34692  fvineqsneq  34695  pibt2  34700  sdclem2  35019  heibor1lem  35089  grpomndo  35155  prtlem9  36002  prter1  36017  prter2  36019  hl2at  36543  cvrval4N  36552  athgt  36594  1dimN  36609  lhpexnle  37144  lhpexle1  37146  cdlemftr2  37704  cdlemftr1  37705  cdlemftr0  37706  cdlemg5  37743  cdlemg33c0  37840  mapdrvallem2  38783  eldiophb  39361  rmxyelqirr  39514  hbtlem1  39730  hbtlem7  39732  ss2iundf  40011  mnupwd  40610  iinssf  41414  founiiun  41442  founiiun0  41458  climuzlem  42031  stirlinglem13  42378  fourierdlem112  42510  2reuimp0  43320  2reuimp  43321  gbogbow  43928  sbgoldbo  43959