Theorem reximi 2994

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 2992	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

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:  r19.29d2r  3061  r19.40  3069  reu3  3363  2reu5  3383  ssiun  4498  iinss  4507  elsnxp  5594  elsnxpOLD  5595  elunirn  6413  iiner  7706  erovlem  7730  xpf1o  8007  unbnn2  8102  scott0  8632  dfac2  8836  cflm  8955  alephsing  8981  numthcor  9199  zorng  9209  zornn0g  9210  ttukeyg  9222  uniimadom  9245  axgroth3  9532  qextlt  11908  qextle  11909  mptnn0fsuppd  12660  hash2sspr  13124  cshword  13388  rexanre  13934  climi2  14090  climi0  14091  rlimres  14137  lo1res  14138  caurcvgr  14252  caurcvg2  14256  caucvgb  14258  prodmolem2  14504  prodmo  14505  vdwnnlem1  15537  cshwsiun  15644  isnmnd  17121  efgrelexlemb  17986  nn0gsumfz0  18204  pmatcollpw2lem  20401  eltg2b  20574  neiptopuni  20744  neiptopnei  20746  ordtbas2  20805  lmcvg  20876  cnprest  20903  lmcnp  20918  nrmsep2  20970  bwth  21023  1stcfb  21058  islly2  21097  llycmpkgen  21165  txbas  21180  tx1stc  21263  cnextcn  21681  tmdcn2  21703  utoptop  21848  ucnima  21895  cfiluweak  21909  metrest  22139  metust  22173  cfilucfil  22174  metustbl  22181  xrhmeo  22553  cmetcaulem  22894  iundisj  23123  limcresi  23455  elply2  23756  aalioulem2  23892  ulmf  23940  lgamucov2  24565  2sqlem7  24949  pntrsumbnd  25055  istrkg2ld  25159  tgisline  25322  usgra2edg1  25912  3v3e3cycl1  26172  wwlkn0  26217  1to3vfriendship  26535  2pthfrgrarn  26536  grpoidval  26751  grporcan  26756  grpoinveu  26757  iundisjf  28784  xlt2addrd  28913  xrofsup  28923  iundisjfi  28942  rhmdvdsr  29149  tpr2rico  29286  esumc  29440  esumfsup  29459  esumpcvgval  29467  hasheuni  29474  esumiun  29483  voliune  29619  volfiniune  29620  dya2icoseg2  29667  dya2iocnei  29671  dya2iocuni  29672  omssubaddlem  29688  omssubadd  29689  afsval  30002  bnj31  30039  bnj1239  30130  bnj900  30253  bnj906  30254  bnj1398  30356  bnj1498  30383  colinearex  31337  segcon2  31382  opnrebl2  31486  sdclem2  32708  heibor1lem  32778  grpomndo  32844  2r19.29  33160  prtlem9  33167  prtlem11  33169  prter1  33182  prter2  33184  hl2at  33709  cvrval4N  33718  athgt  33760  1dimN  33775  lhpexnle  34310  lhpexle1  34312  cdlemftr2  34872  cdlemftr1  34873  cdlemftr0  34874  cdlemg5  34911  cdlemg33c0  35008  mapdrvallem2  35952  eldiophb  36338  rmxyelqirr  36493  hbtlem1  36712  hbtlem7  36714  ss2iundf  36970  founiiun  38355  founiiun0  38372  stirlinglem13  38979  fourierdlem112  39111  reuan  39829  2reu2rex  39832  gboagbo  40178  cshword2  40300  umgr2edgneu  40441  umgr3v3e3cycl  41351  eucrctshift  41411  1to3vfriendship-av  41451  2pthfrgrrn  41452  fusgreg2wsp  41500