Theorem reximdva 3202

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
reximdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem reximdva

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  reximddv  3203  reximdvva  3205  reximddv2  3206  wereu2  5577  frpomin  6228  dffo4  6961  nnaordex  8431  frfi  8989  fisupg  8992  marypha1  9123  fiinfg  9188  wemapsolem  9239  unwdomg  9273  frmin  9438  rankr1ai  9487  cofsmo  9956  cfcoflem  9959  inar1  10462  nqerf  10617  prlem936  10734  fimaxre  11849  fiminre  11852  arch  12160  bndndx  12162  suprfinzcl  12365  zmin  12613  elpq  12644  qbtwnxr  12863  qsqueeze  12864  qextltlem  12865  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  supxrunb1  12982  ssnn0fi  13633  fsuppmapnn0fiub0  13641  fsuppmapnn0fz  13644  expnlbnd2  13877  r19.29uz  14990  cau3lem  14994  rlim2lt  15134  rlimclim  15183  2clim  15209  o1co  15223  climcn1  15229  climcn2  15230  rlimo1  15254  climsqz  15278  climsqz2  15279  rlimsqzlem  15288  lo1le  15291  climsup  15309  climcau  15310  caucvgrlem2  15314  iseralt  15324  cvgcmp  15456  cvgcmpce  15458  supcvg  15496  rpnnen2lem12  15862  bezoutlem1  16175  divgcdcoprmex  16299  exprmfct  16337  prmdvdsfz  16338  prmdvdsncoprmbd  16359  pclem  16467  pc2dvds  16508  pcprmpw  16512  dvdsprmpweqle  16515  unbenlem  16537  infpnlem2  16540  infpn2  16542  prmunb  16543  vdwlem2  16611  ramub1lem2  16656  prmdvdsprmop  16672  prmgaplem7  16686  ipodrsima  18174  smndex1mgm  18461  grpinveu  18529  dfgrp3lem  18588  psgneu  19029  odbezout  19080  sylow2blem3  19142  nn0gsumfz  19500  ringadd2  19729  irredrmul  19864  lbsextlem2  20336  znunit  20683  mptcoe1fsupp  21296  scmate  21567  scmatscm  21570  scmatfo  21587  mat1scmat  21596  pmatcoe1fsupp  21758  pmatcollpwfi  21839  pmatcollpw3fi  21842  mptcoe1matfsupp  21859  pm2mp  21882  chmaidscmat  21905  cpmadumatpoly  21940  chcoeffeq  21943  cayhamlem3  21944  cayhamlem4  21945  neiptopnei  22191  neitr  22239  cnpnei  22323  haust1  22411  isnrm3  22418  isreg2  22436  tgcmp  22460  hauscmplem  22465  hauscmp  22466  bwth  22469  1stcfb  22504  1stcelcls  22520  lly1stc  22555  txcmplem1  22700  txlm  22707  xkococnlem  22718  filuni  22944  filufint  22979  ufilen  22989  fclscf  23084  cnextcn  23126  ustex2sym  23276  ustex3sym  23277  utopreg  23312  isucn2  23339  ucnima  23341  ucncn  23345  neipcfilu  23356  metequiv2  23572  metrest  23586  xrsmopn  23881  mulc1cncf  23974  cncfco  23976  bndth  24027  lmmcvg  24330  cfil3i  24338  iscau4  24348  cmetcaulem  24357  iscmet3lem1  24360  caussi  24366  equivcfil  24368  equivcau  24369  caubl  24377  minveclem3b  24497  ovolgelb  24549  ovollb2lem  24557  ovolctb  24559  ovolicc2lem4  24589  ioombl1lem4  24630  dyadmax  24667  volsup2  24674  itg2monolem1  24820  c1liplem1  25065  c1lip1  25066  dvivthlem1  25077  lhop1  25083  ftc1a  25106  ftc1lem6  25110  ply1divex  25206  elply2  25262  dgrlem  25295  aacjcl  25392  aalioulem2  25398  aalioulem3  25399  aalioulem4  25400  ulmcaulem  25458  ulmcau  25459  ulmss  25461  mtest  25468  itgulm  25472  reeff1o  25511  efif1olem4  25606  rlimcnp  26020  xrlimcnp  26023  lgamucov  26092  ftalem3  26129  fta  26134  muval1  26187  dvdssqf  26192  mumullem1  26233  lgsqrmod  26405  lgsqrmodndvds  26406  pntlem3  26662  ostth  26692  tgtrisegint  26764  tgbtwndiff  26771  tgcgrxfr  26783  lnext  26832  legov2  26851  legtrd  26854  hlcgrex  26881  colperpexlem3  26997  colperpex  26998  hlpasch  27021  hpgerlem  27030  hpgtr  27033  dfcgra2  27095  acopy  27098  inagswap  27106  inaghl  27110  cgrg3col4  27118  axpasch  27212  wwlksnredwwlkn0  28162  midwwlks2s3  28218  clwwlkn1loopb  28308  2pthfrgrrn2  28548  frgrwopreg1  28583  frgrwopreg2  28584  grpoidinvlem3  28769  grpoideu  28772  grpoinveu  28782  ubthlem1  29133  minvecolem5  29144  htthlem  29180  chscllem2  29901  nmopun  30277  lnconi  30296  rnbra  30370  sumdmdii  30678  cdj3lem2b  30700  foresf1o  30751  acunirnmpt  30898  xrofsup  30992  fprodex01  31041  isarchi3  31343  isarchiofld  31418  lmxrge0  31804  lmdvg  31805  esumlub  31928  esumfsup  31938  esumcvg  31954  ftc2re  32478  cusgr3cyclex  32998  cvmliftmolem2  33144  cvmlift2lem12  33176  satfv1  33225  satffunlem1lem2  33265  satffunlem2lem2  33268  satfv0fvfmla0  33275  wzel  33745  wsuclem  33746  nosupno  33833  nosupbnd1lem4  33841  noinfno  33848  noinfbnd1lem4  33856  conway  33920  etasslt  33934  btwndiff  34256  trisegint  34257  cgrxfr  34284  lineext  34305  segcon2  34334  brsegle2  34338  seglecgr12im  34339  segletr  34343  broutsideof3  34355  opnrebl2  34437  nn0prpw  34439  fin2so  35691  poimirlem27  35731  poimirlem30  35734  poimirlem31  35735  poimir  35737  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  itg2addnclem  35755  ftc1cnnc  35776  ftc1anclem5  35781  sdclem1  35828  geomcau  35844  equivtotbnd  35863  bndss  35871  ismtybndlem  35891  heibor1lem  35894  rrncmslem  35917  rngo2  35992  prtlem15  36816  lsateln0  36936  lsat0cv  36974  eqlkr3  37042  lkrshp  37046  lshpset2N  37060  hlhgt2  37330  hlrelat2  37344  atle  37377  athgt  37397  2dim  37411  1cvratex  37414  ps-2  37419  dalem20  37634  lhpexle1lem  37948  lhpexle1  37949  lhpexle2lem  37950  lhpmcvr5N  37968  lhpmcvr6N  37969  cdleme25a  38294  cdleme29ex  38315  cdlemfnid  38505  cdlemg33b0  38642  cdlemg33a  38647  cdlemg35  38654  cdleml3N  38919  dihlsscpre  39175  dih1dimb2  39182  dihatexv  39279  dvh3dim2  39389  dochkr1  39419  dochkr1OLDN  39420  lcfl8  39443  lcfl8b  39445  lcfrlem5  39487  lcfrlem6  39488  mapdrvallem2  39586  mapdh9a  39730  mapdh9aOLDN  39731  hdmaprnlem3eN  39799  hdmaprnlem16N  39803  flt4lem5elem  40404  flt4lem7  40412  nna4b4nsq  40413  fphpdo  40555  rencldnfilem  40558  irrapxlem2  40561  cvgdvgrat  41820  expgrowth  41842  projf1o  42625  ssfiunibd  42738  supxrgere  42762  supxrgelem  42766  suplesup  42768  infrpge  42780  infleinf  42801  supxrunb3  42829  unb2ltle  42845  uzub  42861  qinioo  42963  qelioo  42974  climinf  43037  mullimc  43047  islptre  43050  limccog  43051  mullimcf  43054  limcrecl  43060  sumnnodd  43061  neglimc  43078  0ellimcdiv  43080  limclner  43082  allbutfifvre  43106  climleltrp  43107  fnlimabslt  43110  climinf2lem  43137  limsuppnflem  43141  limsupvaluz2  43169  supcnvlimsup  43171  limsupgtlem  43208  liminflelimsupuz  43216  liminflimsupclim  43238  limsupub2  43243  xlimpnfxnegmnf  43245  cncfioobd  43328  stoweidlem7  43438  stoweidlem27  43458  stoweidlem39  43470  stoweidlem48  43479  stoweidlem49  43480  stoweidlem60  43491  stoweidlem61  43492  stoweid  43494  dirkercncflem2  43535  fourierdlem20  43558  fourierdlem39  43577  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem64  43601  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem87  43624  fourierdlem103  43640  fourierdlem104  43641  qndenserrnopnlem  43728  sge0ltfirp  43828  sge0gerpmpt  43830  sge0ltfirpmpt2  43854  sge0isum  43855  sge0pnffigtmpt  43868  sge0pnffsumgt  43870  sge0gtfsumgt  43871  sge0uzfsumgt  43872  nnfoctbdjlem  43883  meaiuninclem  43908  meaiuninc3v  43912  omeiunltfirp  43947  carageniuncllem2  43950  hoicvr  43976  volicorescl  43981  hoidmv1le  44022  hoidmvlelem3  44025  hoiqssbllem3  44052  hspmbllem2  44055  iunhoiioolem  44103  vonioo  44110  vonicc  44113  smfaddlem1  44185  smflimlem2  44194  smflimlem3  44195  smfmullem4  44215  fsetsnfo  44434  2reu8i  44492  imasetpreimafvbijlemfo  44745  2pwp1prmfmtno  44930  proththd  44954  sbgoldbwt  45117  sbgoldbst  45118  sbgoldbalt  45121  bgoldbtbndlem4  45148  bgoldbtbnd  45149  zrninitoringc  45517  ply1mulgsumlem3  45617  ply1mulgsumlem4  45618  islindeps2  45712  isldepslvec2  45714