Theorem reximdva 3147

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  reximddv  3150  reximdvva  3186  reximddv2  3197  wereu2  5638  frpomin  6316  dffo4  7078  nnaordex  8605  frfi  9239  fisupg  9242  marypha1  9392  fiinfg  9459  wemapsolem  9510  unwdomg  9544  rankr1ai  9758  cofsmo  10229  cfcoflem  10232  inar1  10735  nqerf  10890  prlem936  11007  fimaxre  12134  fiminre  12137  arch  12446  bndndx  12448  suprfinzcl  12655  zmin  12910  elpq  12941  qbtwnxr  13167  qsqueeze  13168  qextltlem  13169  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  supxrunb1  13286  ssnn0fi  13957  fsuppmapnn0fiub0  13965  fsuppmapnn0fz  13968  expnlbnd2  14206  r19.29uz  15324  cau3lem  15328  rlim2lt  15470  rlimclim  15519  2clim  15545  o1co  15559  climcn1  15565  climcn2  15566  rlimo1  15590  climsqz  15614  climsqz2  15615  rlimsqzlem  15622  lo1le  15625  climsup  15643  climcau  15644  caucvgrlem2  15648  iseralt  15658  cvgcmp  15789  cvgcmpce  15791  supcvg  15829  rpnnen2lem12  16200  bezoutlem1  16516  divgcdcoprmex  16643  exprmfct  16681  prmdvdsfz  16682  prmdvdsncoprmbd  16704  pclem  16816  pc2dvds  16857  pcprmpw  16861  dvdsprmpweqle  16864  unbenlem  16886  infpnlem2  16889  infpn2  16891  prmunb  16892  vdwlem2  16960  ramub1lem2  17005  prmdvdsprmop  17021  prmgaplem7  17035  ipodrsima  18507  smndex1mgm  18841  grpinveu  18913  dfgrp3lem  18977  psgneu  19443  odbezout  19495  sylow2blem3  19559  nn0gsumfz  19921  irredrmul  20343  zrninitoringc  20592  lbsextlem2  21076  znunit  21480  mptcoe1fsupp  22107  evls1fpws  22263  scmate  22404  scmatscm  22407  scmatfo  22424  mat1scmat  22433  pmatcoe1fsupp  22595  pmatcollpwfi  22676  pmatcollpw3fi  22679  mptcoe1matfsupp  22696  pm2mp  22719  chmaidscmat  22742  cpmadumatpoly  22777  chcoeffeq  22780  cayhamlem3  22781  cayhamlem4  22782  neiptopnei  23026  neitr  23074  cnpnei  23158  haust1  23246  isnrm3  23253  isreg2  23271  tgcmp  23295  hauscmplem  23300  hauscmp  23301  bwth  23304  1stcfb  23339  1stcelcls  23355  lly1stc  23390  txcmplem1  23535  txlm  23542  xkococnlem  23553  filuni  23779  filufint  23814  ufilen  23824  fclscf  23919  cnextcn  23961  ustex2sym  24111  ustex3sym  24112  utopreg  24147  isucn2  24173  ucnima  24175  ucncn  24179  neipcfilu  24190  metequiv2  24405  metrest  24419  xrsmopn  24708  mulc1cncf  24805  cncfco  24807  bndth  24864  lmmcvg  25168  cfil3i  25176  iscau4  25186  cmetcaulem  25195  iscmet3lem1  25198  caussi  25204  equivcfil  25206  equivcau  25207  caubl  25215  minveclem3b  25335  ovolgelb  25388  ovollb2lem  25396  ovolctb  25398  ovolicc2lem4  25428  ioombl1lem4  25469  dyadmax  25506  volsup2  25513  itg2monolem1  25658  c1liplem1  25908  c1lip1  25909  dvivthlem1  25920  lhop1  25926  ftc1a  25951  ftc1lem6  25955  ply1divex  26049  elply2  26108  dgrlem  26141  aacjcl  26242  aalioulem2  26248  aalioulem3  26249  aalioulem4  26250  ulmcaulem  26310  ulmcau  26311  ulmss  26313  mtest  26320  itgulm  26324  reeff1o  26364  efif1olem4  26461  rlimcnp  26882  xrlimcnp  26885  lgamucov  26955  ftalem3  26992  fta  26997  muval1  27050  dvdssqf  27055  mumullem1  27096  lgsqrmod  27270  lgsqrmodndvds  27271  pntlem3  27527  ostth  27557  nosupno  27622  nosupbnd1lem4  27630  noinfno  27637  noinfbnd1lem4  27645  conway  27718  etasslt  27732  znegscl  28287  tgtrisegint  28433  tgbtwndiff  28440  tgcgrxfr  28452  lnext  28501  legov2  28520  legtrd  28523  hlcgrex  28550  colperpexlem3  28666  colperpex  28667  hlpasch  28690  hpgerlem  28699  hpgtr  28702  dfcgra2  28764  acopy  28767  inagswap  28775  inaghl  28779  cgrg3col4  28787  axpasch  28875  wwlksnredwwlkn0  29833  midwwlks2s3  29889  clwwlkn1loopb  29979  2pthfrgrrn2  30219  frgrwopreg1  30254  frgrwopreg2  30255  grpoidinvlem3  30442  grpoideu  30445  grpoinveu  30455  ubthlem1  30806  minvecolem5  30817  htthlem  30853  chscllem2  31574  nmopun  31950  lnconi  31969  rnbra  32043  sumdmdii  32351  cdj3lem2b  32373  foresf1o  32440  acunirnmpt  32590  xrofsup  32697  fprodex01  32757  mndlactfo  32975  mndractfo  32977  isarchi3  33148  erler  33223  isarchiofld  33302  dfufd2lem  33527  constrconj  33742  constrextdg2lem  33745  constrcjcl  33765  lmxrge0  33949  lmdvg  33950  esumlub  34057  esumfsup  34067  esumcvg  34083  ftc2re  34596  cusgr3cyclex  35130  cvmliftmolem2  35276  cvmlift2lem12  35308  satfv1  35357  satffunlem1lem2  35397  satffunlem2lem2  35400  satfv0fvfmla0  35407  ellcsrspsn  35635  r1peuqusdeg1  35637  wzel  35819  wsuclem  35820  btwndiff  36022  trisegint  36023  cgrxfr  36050  lineext  36071  segcon2  36100  brsegle2  36104  seglecgr12im  36105  segletr  36109  broutsideof3  36121  opnrebl2  36316  nn0prpw  36318  fin2so  37608  poimirlem27  37648  poimirlem30  37651  poimirlem31  37652  poimir  37654  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem  37672  ftc1cnnc  37693  ftc1anclem5  37698  sdclem1  37744  geomcau  37760  equivtotbnd  37779  bndss  37787  ismtybndlem  37807  heibor1lem  37810  rrncmslem  37833  rngo2  37908  prtlem15  38875  lsateln0  38995  lsat0cv  39033  eqlkr3  39101  lkrshp  39105  lshpset2N  39119  hlhgt2  39390  hlrelat2  39404  atle  39437  athgt  39457  2dim  39471  1cvratex  39474  ps-2  39479  dalem20  39694  lhpexle1lem  40008  lhpexle1  40009  lhpexle2lem  40010  lhpmcvr5N  40028  lhpmcvr6N  40029  cdleme25a  40354  cdleme29ex  40375  cdlemfnid  40565  cdlemg33b0  40702  cdlemg33a  40707  cdlemg35  40714  cdleml3N  40979  dihlsscpre  41235  dih1dimb2  41242  dihatexv  41339  dvh3dim2  41449  dochkr1  41479  dochkr1OLDN  41480  lcfl8  41503  lcfl8b  41505  lcfrlem5  41547  lcfrlem6  41548  mapdrvallem2  41646  mapdh9a  41790  mapdh9aOLDN  41791  hdmaprnlem3eN  41859  hdmaprnlem16N  41863  mndmolinv  42090  primrootsunit1  42092  flt4lem5elem  42646  flt4lem7  42654  nna4b4nsq  42655  fphpdo  42812  rencldnfilem  42815  irrapxlem2  42818  oasubex  43282  tfsconcatlem  43332  tfsconcatrev  43344  cvgdvgrat  44309  expgrowth  44331  projf1o  45198  ssfiunibd  45314  supxrgere  45336  supxrgelem  45340  suplesup  45342  infrpge  45354  infleinf  45375  supxrunb3  45402  unb2ltle  45418  uzub  45434  cvgcaule  45494  qinioo  45540  qelioo  45551  climinf  45611  mullimc  45621  islptre  45624  limccog  45625  mullimcf  45628  limcrecl  45634  sumnnodd  45635  neglimc  45652  0ellimcdiv  45654  limclner  45656  allbutfifvre  45680  climleltrp  45681  fnlimabslt  45684  climinf2lem  45711  limsuppnflem  45715  limsupvaluz2  45743  supcnvlimsup  45745  limsupgtlem  45782  liminflelimsupuz  45790  liminflimsupclim  45812  limsupub2  45817  xlimpnfxnegmnf  45819  cncfioobd  45902  stoweidlem7  46012  stoweidlem27  46032  stoweidlem39  46044  stoweidlem48  46053  stoweidlem49  46054  stoweidlem60  46065  stoweidlem61  46066  stoweid  46068  dirkercncflem2  46109  fourierdlem20  46132  fourierdlem39  46151  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem64  46175  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  qndenserrnopnlem  46302  sge0ltfirp  46405  sge0gerpmpt  46407  sge0ltfirpmpt2  46431  sge0isum  46432  sge0pnffigtmpt  46445  sge0pnffsumgt  46447  sge0gtfsumgt  46448  sge0uzfsumgt  46449  nnfoctbdjlem  46460  meaiuninclem  46485  meaiuninc3v  46489  omeiunltfirp  46524  carageniuncllem2  46527  hoicvr  46553  volicorescl  46558  hoidmv1le  46599  hoidmvlelem3  46602  hoiqssbllem3  46629  hspmbllem2  46632  iunhoiioolem  46680  vonioo  46687  vonicc  46690  smfaddlem1  46768  smflimlem2  46777  smflimlem3  46778  smfmullem4  46799  fsetsnfo  47058  2reu8i  47118  imasetpreimafvbijlemfo  47410  2pwp1prmfmtno  47595  proththd  47619  sbgoldbwt  47782  sbgoldbst  47783  sbgoldbalt  47786  bgoldbtbndlem4  47813  bgoldbtbnd  47814  grtriprop  47944  ply1mulgsumlem3  48381  ply1mulgsumlem4  48382  islindeps2  48476  isldepslvec2  48478