Theorem reximdva 3177

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 418	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3175	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089

This theorem is used by:  reximddv  3180  reximdvva  3212  reximddv2  3223  wereu2  5656  frpomin  6342  dffo4  7100  nnaordex  8630  frfi  9259  fisupg  9262  marypha1  9408  fiinfg  9475  wemapsolem  9526  unwdomg  9560  rankr1ai  9784  cofsmo  10275  cfcoflem  10278  inar1  10788  nqerf  10943  prlem936  11060  fimaxre  12187  fiminre  12190  arch  12529  bndndx  12531  suprfinzcl  12739  zmin  12997  elpq  13029  qbtwnxr  13256  qsqueeze  13257  qextltlem  13258  xrsupsslem  13363  xrinfmsslem  13364  xrub  13368  supxrunb1  13375  ssnn0fi  14053  fsuppmapnn0fiub0  14061  fsuppmapnn0fz  14064  expnlbnd2  14302  r19.29uz  15442  cau3lem  15446  rlim2lt  15588  rlimclim  15637  2clim  15663  o1co  15677  climcn1  15683  climcn2  15684  rlimo1  15708  climsqz  15732  climsqz2  15733  rlimsqzlem  15740  lo1le  15743  climsup  15761  climcau  15762  caucvgrlem2  15766  iseralt  15776  cvgcmp  15907  cvgcmpce  15909  supcvg  15949  rpnnen2lem12  16319  bezoutlem1  16635  divgcdcoprmex  16762  exprmfct  16801  prmdvdsfz  16802  prmdvdsncoprmbd  16824  pclem  16936  pc2dvds  16977  pcprmpw  16981  dvdsprmpweqle  16984  unbenlem  17006  infpnlem2  17009  infpn2  17011  prmunb  17012  vdwlem2  17080  ramub1lem2  17125  prmdvdsprmop  17141  prmgaplem7  17155  ipodrsima  18635  smndex1mgm  19025  grpinveu  19104  dfgrp3lem  19167  psgneu  19639  odbezout  19691  sylow2blem3  19755  nn0gsumfz  20117  irredrmul  20574  zrninitoringc  20844  lbsextlem2  21352  znunit  21782  mptcoe1fsupp  22446  evls1fpws  22600  scmate  22738  scmatscm  22741  scmatfo  22758  mat1scmat  22767  pmatcoe1fsupp  22932  pmatcollpwfi  23013  pmatcollpw3fi  23016  mptcoe1matfsupp  23033  pm2mp  23056  chmaidscmat  23079  cpmadumatpoly  23114  chcoeffeq  23117  cayhamlem3  23118  cayhamlem4  23119  neiptopnei  23363  neitr  23411  cnpnei  23495  haust1  23583  isnrm3  23590  isreg2  23608  tgcmp  23632  hauscmplem  23637  hauscmp  23638  bwth  23641  1stcfb  23676  1stcelcls  23693  lly1stc  23728  txcmplem1  23873  txlm  23880  xkococnlem  23891  filuni  24117  filufint  24152  ufilen  24162  fclscf  24257  cnextcn  24299  ustex2sym  24449  ustex3sym  24450  utopreg  24484  isucn2  24510  ucnima  24512  ucncn  24516  neipcfilu  24527  metequiv2  24742  metrest  24756  xrsmopn  25045  mulc1cncf  25139  cncfco  25141  bndth  25192  lmmcvg  25495  cfil3i  25503  iscau4  25513  cmetcaulem  25522  iscmet3lem1  25525  caussi  25531  equivcfil  25533  equivcau  25534  caubl  25542  minveclem3b  25662  ovolgelb  25714  ovollb2lem  25722  ovolctb  25724  ovolicc2lem4  25754  ioombl1lem4  25795  dyadmax  25832  volsup2  25839  itg2monolem1  25984  c1liplem1  26230  c1lip1  26231  dvivthlem1  26242  lhop1  26248  ftc1a  26271  ftc1lem6  26275  ply1divex  26369  elply2  26428  dgrlem  26462  aacjcl  26570  aalioulem2  26576  aalioulem3  26577  aalioulem4  26578  ulmcaulem  26637  ulmcau  26638  ulmss  26640  mtest  26647  itgulm  26651  reeff1o  26690  efif1olem4  26790  rlimcnp  27210  xrlimcnp  27213  lgamucov  27282  ftalem3  27319  fta  27324  muval1  27377  dvdssqf  27382  mumullem1  27423  lgsqrmod  27596  lgsqrmodndvds  27597  pntlem3  27853  ostth  27883  nosupno  27947  nosupbnd1lem4  27955  noinfno  27962  noinfbnd1lem4  27970  conway  28052  etaslts  28066  znegscl  28665  tgtrisegint  28849  tgbtwndiff  28856  tgcgrxfr  28868  lnext  28917  legov2  28936  legtrd  28939  hlcgrex  28969  colperpexlem3  29095  colperpex  29096  hlpasch  29121  hpgerlem  29130  hpgtr  29133  dfcgra2  29225  acopy  29228  inagswap  29247  inaghl  29251  cgrg3col4  29259  axpasch  29406  wwlksnredwwlkn0  30372  midwwlks2s3  30428  clwwlkn1loopb  30521  2pthfrgrrn2  30771  frgrwopreg1  30806  frgrwopreg2  30807  grpoidinvlem3  30995  grpoideu  30998  grpoinveu  31008  ubthlem1  31359  minvecolem5  31370  htthlem  31406  chscllem2  32127  nmopun  32503  lnconi  32522  rnbra  32596  sumdmdii  32904  cdj3lem2b  32926  foresf1o  32987  acunirnmpt  33140  xrofsup  33246  fprodex01  33303  mndlactfo  33475  mndractfo  33477  isarchi3  33635  isarchiofld  33647  erler  33713  erld2  33714  dfufd2lem  33967  constrconj  34263  constrextdg2lem  34266  constrcjcl  34286  lmxrge0  34470  lmdvg  34471  esumlub  34578  esumfsup  34588  esumcvg  34604  ftc2re  35114  cusgr3cyclex  35733  cvmliftmolem2  35869  cvmlift2lem12  35901  satfv1  35950  satffunlem1lem2  35990  satffunlem2lem2  35993  satfv0fvfmla0  36000  ellcsrspsn  36228  r1peuqusdeg1  36230  wzel  36409  wsuclem  36410  btwndiff  36615  trisegint  36616  cgrxfr  36643  lineext  36664  segcon2  36693  brsegle2  36697  seglecgr12im  36698  segletr  36702  broutsideof3  36714  opnrebl2  36948  nn0prpw  36950  fin2so  38369  poimirlem27  38404  poimirlem30  38407  poimirlem31  38408  poimir  38410  mblfinlem1  38414  mblfinlem2  38415  mblfinlem3  38416  mblfinlem4  38417  itg2addnclem  38428  ftc1cnnc  38449  ftc1anclem5  38454  sdclem1  38501  geomcau  38517  equivtotbnd  38536  bndss  38544  ismtybndlem  38564  heibor1lem  38567  rrncmslem  38590  rngo2  38665  prtlem15  39756  lsateln0  39876  lsat0cv  39914  eqlkr3  39982  lkrshp  39986  lshpset2N  40000  hlhgt2  40270  hlrelat2  40284  atle  40317  athgt  40337  2dim  40351  1cvratex  40354  ps-2  40359  dalem20  40574  lhpexle1lem  40888  lhpexle1  40889  lhpexle2lem  40890  lhpmcvr5N  40908  lhpmcvr6N  40909  cdleme25a  41234  cdleme29ex  41255  cdlemfnid  41445  cdlemg33b0  41582  cdlemg33a  41587  cdlemg35  41594  cdleml3N  41859  dihlsscpre  42115  dih1dimb2  42122  dihatexv  42219  dvh3dim2  42329  dochkr1  42359  dochkr1OLDN  42360  lcfl8  42383  lcfl8b  42385  lcfrlem5  42427  lcfrlem6  42428  mapdrvallem2  42526  mapdh9a  42670  mapdh9aOLDN  42671  hdmaprnlem3eN  42739  hdmaprnlem16N  42743  mndmolinv  42969  primrootsunit1  42971  flt4lem5elem  43505  flt4lem7  43513  nna4b4nsq  43514  fphpdo  43666  rencldnfilem  43669  irrapxlem2  43672  oasubex  44135  tfsconcatlem  44185  tfsconcatrev  44197  cvgdvgrat  45145  expgrowth  45167  projf1o  46036  ssfiunibd  46150  supxrgere  46171  supxrgelem  46175  suplesup  46177  infrpge  46189  infleinf  46209  supxrunb3  46236  unb2ltle  46251  uzub  46267  cvgcaule  46327  qinioo  46373  qelioo  46384  climinf  46444  mullimc  46454  islptre  46457  limccog  46458  mullimcf  46461  limcrecl  46467  sumnnodd  46468  neglimc  46483  0ellimcdiv  46485  limclner  46487  allbutfifvre  46511  climleltrp  46512  fnlimabslt  46515  climinf2lem  46542  limsuppnflem  46546  limsupvaluz2  46574  supcnvlimsup  46576  limsupgtlem  46613  liminflelimsupuz  46621  liminflimsupclim  46643  limsupub2  46648  xlimpnfxnegmnf  46650  cncfioobd  46733  stoweidlem7  46843  stoweidlem27  46863  stoweidlem39  46875  stoweidlem48  46884  stoweidlem49  46885  stoweidlem60  46896  stoweidlem61  46897  stoweid  46899  dirkercncflem2  46940  fourierdlem20  46963  fourierdlem39  46982  fourierdlem41  46984  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem64  47006  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem87  47029  fourierdlem103  47045  fourierdlem104  47046  qndenserrnopnlem  47133  sge0ltfirp  47236  sge0gerpmpt  47238  sge0ltfirpmpt2  47262  sge0isum  47263  sge0pnffigtmpt  47276  sge0pnffsumgt  47278  sge0gtfsumgt  47279  sge0uzfsumgt  47280  nnfoctbdjlem  47291  meaiuninclem  47316  meaiuninc3v  47320  omeiunltfirp  47355  carageniuncllem2  47358  volicorescl  47389  hoidmv1le  47430  hoidmvlelem3  47433  hoiqssbllem3  47460  hspmbllem2  47463  iunhoiioolem  47511  vonioo  47518  vonicc  47521  smfaddlem1  47599  smflimlem2  47608  smflimlem3  47609  smfmullem4  47630  fsetsnfo  47949  2reu8i  48009  imasetpreimafvbijlemfo  48313  2pwp1prmfmtno  48501  proththd  48525  sbgoldbwt  48701  sbgoldbst  48702  sbgoldbalt  48705  bgoldbtbndlem4  48732  bgoldbtbnd  48733  grtriprop  48865  ply1mulgsumlem3  49326  ply1mulgsumlem4  49327  islindeps2  49421  isldepslvec2  49423