Theorem reximi 3207

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

Syntax hints:   → wi 4   ∈ wcel 2081  ∃wrex 3106

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-ral 3110  df-rex 3111

This theorem is referenced by:  r19.29r  3219  2r19.29  3295  r19.29d2r  3296  r19.29vva  3297  r19.35  3302  r19.40  3307  2reu2rex  3392  reu3  3652  2reu5  3683  reuan  3808  ssiun  4869  iinss  4879  elsnxp  6017  elunirn  6875  iiner  8219  erovlem  8243  xpf1o  8526  unbnn2  8621  scott0  9161  dfac2b  9402  cflm  9518  alephsing  9544  numthcor  9762  zorng  9772  zornn0g  9773  ttukeyg  9785  uniimadom  9812  axgroth3  10099  qextlt  12446  qextle  12447  mptnn0fsuppd  13216  hashgt23el  13633  hash2sspr  13692  cshword  13989  rexanre  14540  climi2  14702  climi0  14703  rlimres  14749  lo1res  14750  caurcvgr  14864  caurcvg2  14868  caucvgb  14870  prodmolem2  15122  prodmo  15123  vdwnnlem1  16160  cshwsiun  16262  isnmnd  17737  efgrelexlemb  18603  nn0gsumfz0  18822  pmatcollpw2lem  21069  eltg2b  21251  neiptopuni  21422  neiptopnei  21424  ordtbas2  21483  lmcvg  21554  cnprest  21581  lmcnp  21596  nrmsep2  21648  bwth  21702  1stcfb  21737  islly2  21776  llycmpkgen  21844  txbas  21859  tx1stc  21942  cnextcn  22359  tmdcn2  22381  utoptop  22526  ucnima  22573  cfiluweak  22587  metrest  22817  metust  22851  cfilucfil  22852  metustbl  22859  xrhmeo  23233  cmetcaulem  23574  iundisj  23832  limcresi  24166  elply2  24469  aalioulem2  24605  ulmf  24653  lgamucov2  25298  2sqlem7  25682  2sqreultblem  25706  2sqreunnltblem  25709  pntrsumbnd  25824  istrkg2ld  25928  tgisline  26095  umgr2edgneu  26679  umgr3v3e3cycl  27650  eucrctshift  27710  1to3vfriendship  27752  2pthfrgrrn  27753  grpoidval  27981  grporcan  27986  grpoinveu  27987  iunrnmptss  30007  iundisjf  30029  xlt2addrd  30170  xrofsup  30180  iundisjfi  30205  rhmdvdsr  30545  tpr2rico  30772  esumc  30927  esumfsup  30946  esumpcvgval  30954  hasheuni  30961  esumiun  30970  voliune  31105  volfiniune  31106  dya2icoseg2  31153  dya2iocnei  31157  dya2iocuni  31158  omssubaddlem  31174  omssubadd  31175  afsval  31559  bnj31  31606  bnj1239  31694  bnj900  31817  bnj906  31818  bnj1398  31920  bnj1498  31947  satfvsuclem1  32215  satfv1  32219  satfvsucsuc  32221  nosupno  32813  nosupfv  32816  colinearex  33131  segcon2  33176  opnrebl2  33279  nlpfvineqsn  34240  fvineqsneq  34243  pibt2  34248  sdclem2  34568  heibor1lem  34638  grpomndo  34704  prtlem9  35550  prter1  35565  prter2  35567  hl2at  36091  cvrval4N  36100  athgt  36142  1dimN  36157  lhpexnle  36692  lhpexle1  36694  cdlemftr2  37252  cdlemftr1  37253  cdlemftr0  37254  cdlemg5  37291  cdlemg33c0  37388  mapdrvallem2  38331  eldiophb  38858  rmxyelqirr  39011  hbtlem1  39227  hbtlem7  39229  ss2iundf  39508  mnupwd  40119  ablsimpgfind  40186  iinssf  40965  founiiun  40994  founiiun0  41010  climuzlem  41585  stirlinglem13  41933  fourierdlem112  42065  2reuimp0  42849  2reuimp  42850  gbogbow  43423  sbgoldbo  43454