Theorem reximdva 3150

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
ralimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		ralimdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 412	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3148	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  reximddv  3153  reximdvva  3185  reximddv2  3196  wereu2  5628  frpomin  6304  dffo4  7055  nnaordex  8574  frfi  9195  fisupg  9198  marypha1  9347  fiinfg  9414  wemapsolem  9465  unwdomg  9499  rankr1ai  9722  cofsmo  10191  cfcoflem  10194  inar1  10698  nqerf  10853  prlem936  10970  fimaxre  12100  fiminre  12103  arch  12434  bndndx  12436  suprfinzcl  12643  zmin  12894  elpq  12925  qbtwnxr  13152  qsqueeze  13153  qextltlem  13154  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  supxrunb1  13271  ssnn0fi  13947  fsuppmapnn0fiub0  13955  fsuppmapnn0fz  13958  expnlbnd2  14196  r19.29uz  15313  cau3lem  15317  rlim2lt  15459  rlimclim  15508  2clim  15534  o1co  15548  climcn1  15554  climcn2  15555  rlimo1  15579  climsqz  15603  climsqz2  15604  rlimsqzlem  15611  lo1le  15614  climsup  15632  climcau  15633  caucvgrlem2  15637  iseralt  15647  cvgcmp  15779  cvgcmpce  15781  supcvg  15821  rpnnen2lem12  16192  bezoutlem1  16508  divgcdcoprmex  16635  exprmfct  16674  prmdvdsfz  16675  prmdvdsncoprmbd  16697  pclem  16809  pc2dvds  16850  pcprmpw  16854  dvdsprmpweqle  16857  unbenlem  16879  infpnlem2  16882  infpn2  16884  prmunb  16885  vdwlem2  16953  ramub1lem2  16998  prmdvdsprmop  17014  prmgaplem7  17028  ipodrsima  18507  smndex1mgm  18878  grpinveu  18950  dfgrp3lem  19014  psgneu  19481  odbezout  19533  sylow2blem3  19597  nn0gsumfz  19959  irredrmul  20407  zrninitoringc  20653  lbsextlem2  21157  znunit  21543  mptcoe1fsupp  22179  evls1fpws  22334  scmate  22475  scmatscm  22478  scmatfo  22495  mat1scmat  22504  pmatcoe1fsupp  22666  pmatcollpwfi  22747  pmatcollpw3fi  22750  mptcoe1matfsupp  22767  pm2mp  22790  chmaidscmat  22813  cpmadumatpoly  22848  chcoeffeq  22851  cayhamlem3  22852  cayhamlem4  22853  neiptopnei  23097  neitr  23145  cnpnei  23229  haust1  23317  isnrm3  23324  isreg2  23342  tgcmp  23366  hauscmplem  23371  hauscmp  23372  bwth  23375  1stcfb  23410  1stcelcls  23426  lly1stc  23461  txcmplem1  23606  txlm  23613  xkococnlem  23624  filuni  23850  filufint  23885  ufilen  23895  fclscf  23990  cnextcn  24032  ustex2sym  24182  ustex3sym  24183  utopreg  24217  isucn2  24243  ucnima  24245  ucncn  24249  neipcfilu  24260  metequiv2  24475  metrest  24489  xrsmopn  24778  mulc1cncf  24872  cncfco  24874  bndth  24925  lmmcvg  25228  cfil3i  25236  iscau4  25246  cmetcaulem  25255  iscmet3lem1  25258  caussi  25264  equivcfil  25266  equivcau  25267  caubl  25275  minveclem3b  25395  ovolgelb  25447  ovollb2lem  25455  ovolctb  25457  ovolicc2lem4  25487  ioombl1lem4  25528  dyadmax  25565  volsup2  25572  itg2monolem1  25717  c1liplem1  25963  c1lip1  25964  dvivthlem1  25975  lhop1  25981  ftc1a  26004  ftc1lem6  26008  ply1divex  26102  elply2  26161  dgrlem  26194  aacjcl  26293  aalioulem2  26299  aalioulem3  26300  aalioulem4  26301  ulmcaulem  26359  ulmcau  26360  ulmss  26362  mtest  26369  itgulm  26373  reeff1o  26412  efif1olem4  26509  rlimcnp  26929  xrlimcnp  26932  lgamucov  27001  ftalem3  27038  fta  27043  muval1  27096  dvdssqf  27101  mumullem1  27142  lgsqrmod  27315  lgsqrmodndvds  27316  pntlem3  27572  ostth  27602  nosupno  27667  nosupbnd1lem4  27675  noinfno  27682  noinfbnd1lem4  27690  conway  27771  etaslts  27785  znegscl  28384  tgtrisegint  28567  tgbtwndiff  28574  tgcgrxfr  28586  lnext  28635  legov2  28654  legtrd  28657  hlcgrex  28684  colperpexlem3  28800  colperpex  28801  hlpasch  28824  hpgerlem  28833  hpgtr  28836  dfcgra2  28898  acopy  28901  inagswap  28909  inaghl  28913  cgrg3col4  28921  axpasch  29010  wwlksnredwwlkn0  29964  midwwlks2s3  30020  clwwlkn1loopb  30113  2pthfrgrrn2  30353  frgrwopreg1  30388  frgrwopreg2  30389  grpoidinvlem3  30577  grpoideu  30580  grpoinveu  30590  ubthlem1  30941  minvecolem5  30952  htthlem  30988  chscllem2  31709  nmopun  32085  lnconi  32104  rnbra  32178  sumdmdii  32486  cdj3lem2b  32508  foresf1o  32574  acunirnmpt  32732  xrofsup  32840  fprodex01  32898  mndlactfo  33087  mndractfo  33089  isarchi3  33248  isarchiofld  33260  erler  33326  dfufd2lem  33609  constrconj  33889  constrextdg2lem  33892  constrcjcl  33912  lmxrge0  34096  lmdvg  34097  esumlub  34204  esumfsup  34214  esumcvg  34230  ftc2re  34742  cusgr3cyclex  35318  cvmliftmolem2  35464  cvmlift2lem12  35496  satfv1  35545  satffunlem1lem2  35585  satffunlem2lem2  35588  satfv0fvfmla0  35595  ellcsrspsn  35823  r1peuqusdeg1  35825  wzel  36004  wsuclem  36005  btwndiff  36209  trisegint  36210  cgrxfr  36237  lineext  36258  segcon2  36287  brsegle2  36291  seglecgr12im  36292  segletr  36296  broutsideof3  36308  opnrebl2  36503  nn0prpw  36505  fin2so  37928  poimirlem27  37968  poimirlem30  37971  poimirlem31  37972  poimir  37974  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem  37992  ftc1cnnc  38013  ftc1anclem5  38018  sdclem1  38064  geomcau  38080  equivtotbnd  38099  bndss  38107  ismtybndlem  38127  heibor1lem  38130  rrncmslem  38153  rngo2  38228  prtlem15  39321  lsateln0  39441  lsat0cv  39479  eqlkr3  39547  lkrshp  39551  lshpset2N  39565  hlhgt2  39835  hlrelat2  39849  atle  39882  athgt  39902  2dim  39916  1cvratex  39919  ps-2  39924  dalem20  40139  lhpexle1lem  40453  lhpexle1  40454  lhpexle2lem  40455  lhpmcvr5N  40473  lhpmcvr6N  40474  cdleme25a  40799  cdleme29ex  40820  cdlemfnid  41010  cdlemg33b0  41147  cdlemg33a  41152  cdlemg35  41159  cdleml3N  41424  dihlsscpre  41680  dih1dimb2  41687  dihatexv  41784  dvh3dim2  41894  dochkr1  41924  dochkr1OLDN  41925  lcfl8  41948  lcfl8b  41950  lcfrlem5  41992  lcfrlem6  41993  mapdrvallem2  42091  mapdh9a  42235  mapdh9aOLDN  42236  hdmaprnlem3eN  42304  hdmaprnlem16N  42308  mndmolinv  42534  primrootsunit1  42536  flt4lem5elem  43084  flt4lem7  43092  nna4b4nsq  43093  fphpdo  43245  rencldnfilem  43248  irrapxlem2  43251  oasubex  43714  tfsconcatlem  43764  tfsconcatrev  43776  cvgdvgrat  44740  expgrowth  44762  projf1o  45626  ssfiunibd  45742  supxrgere  45763  supxrgelem  45767  suplesup  45769  infrpge  45781  infleinf  45801  supxrunb3  45828  unb2ltle  45843  uzub  45859  cvgcaule  45919  qinioo  45965  qelioo  45976  climinf  46036  mullimc  46046  islptre  46049  limccog  46050  mullimcf  46053  limcrecl  46059  sumnnodd  46060  neglimc  46075  0ellimcdiv  46077  limclner  46079  allbutfifvre  46103  climleltrp  46104  fnlimabslt  46107  climinf2lem  46134  limsuppnflem  46138  limsupvaluz2  46166  supcnvlimsup  46168  limsupgtlem  46205  liminflelimsupuz  46213  liminflimsupclim  46235  limsupub2  46240  xlimpnfxnegmnf  46242  cncfioobd  46325  stoweidlem7  46435  stoweidlem27  46455  stoweidlem39  46467  stoweidlem48  46476  stoweidlem49  46477  stoweidlem60  46488  stoweidlem61  46489  stoweid  46491  dirkercncflem2  46532  fourierdlem20  46555  fourierdlem39  46574  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem64  46598  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  qndenserrnopnlem  46725  sge0ltfirp  46828  sge0gerpmpt  46830  sge0ltfirpmpt2  46854  sge0isum  46855  sge0pnffigtmpt  46868  sge0pnffsumgt  46870  sge0gtfsumgt  46871  sge0uzfsumgt  46872  nnfoctbdjlem  46883  meaiuninclem  46908  meaiuninc3v  46912  omeiunltfirp  46947  carageniuncllem2  46950  volicorescl  46981  hoidmv1le  47022  hoidmvlelem3  47025  hoiqssbllem3  47052  hspmbllem2  47055  iunhoiioolem  47103  vonioo  47110  vonicc  47113  smfaddlem1  47191  smflimlem2  47200  smflimlem3  47201  smfmullem4  47222  fsetsnfo  47501  2reu8i  47561  imasetpreimafvbijlemfo  47865  2pwp1prmfmtno  48053  proththd  48077  sbgoldbwt  48253  sbgoldbst  48254  sbgoldbalt  48257  bgoldbtbndlem4  48284  bgoldbtbnd  48285  grtriprop  48417  ply1mulgsumlem3  48864  ply1mulgsumlem4  48865  islindeps2  48959  isldepslvec2  48961