Theorem reximdva 3166

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  ∃wrex 3068

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069

This theorem is referenced by:  reximddv  3169  reximdvva  3203  reximddv2  3210  wereu2  5672  frpomin  6340  dffo4  7103  nnaordex  8640  frfi  9290  fisupg  9293  marypha1  9431  fiinfg  9496  wemapsolem  9547  unwdomg  9581  rankr1ai  9795  cofsmo  10266  cfcoflem  10269  inar1  10772  nqerf  10927  prlem936  11044  fimaxre  12162  fiminre  12165  arch  12473  bndndx  12475  suprfinzcl  12680  zmin  12932  elpq  12963  qbtwnxr  13183  qsqueeze  13184  qextltlem  13185  xrsupsslem  13290  xrinfmsslem  13291  xrub  13295  supxrunb1  13302  ssnn0fi  13954  fsuppmapnn0fiub0  13962  fsuppmapnn0fz  13965  expnlbnd2  14201  r19.29uz  15301  cau3lem  15305  rlim2lt  15445  rlimclim  15494  2clim  15520  o1co  15534  climcn1  15540  climcn2  15541  rlimo1  15565  climsqz  15589  climsqz2  15590  rlimsqzlem  15599  lo1le  15602  climsup  15620  climcau  15621  caucvgrlem2  15625  iseralt  15635  cvgcmp  15766  cvgcmpce  15768  supcvg  15806  rpnnen2lem12  16172  bezoutlem1  16485  divgcdcoprmex  16607  exprmfct  16645  prmdvdsfz  16646  prmdvdsncoprmbd  16667  pclem  16775  pc2dvds  16816  pcprmpw  16820  dvdsprmpweqle  16823  unbenlem  16845  infpnlem2  16848  infpn2  16850  prmunb  16851  vdwlem2  16919  ramub1lem2  16964  prmdvdsprmop  16980  prmgaplem7  16994  ipodrsima  18498  smndex1mgm  18824  grpinveu  18895  dfgrp3lem  18957  psgneu  19415  odbezout  19467  sylow2blem3  19531  nn0gsumfz  19893  irredrmul  20318  lbsextlem2  20917  znunit  21338  mptcoe1fsupp  21958  scmate  22232  scmatscm  22235  scmatfo  22252  mat1scmat  22261  pmatcoe1fsupp  22423  pmatcollpwfi  22504  pmatcollpw3fi  22507  mptcoe1matfsupp  22524  pm2mp  22547  chmaidscmat  22570  cpmadumatpoly  22605  chcoeffeq  22608  cayhamlem3  22609  cayhamlem4  22610  neiptopnei  22856  neitr  22904  cnpnei  22988  haust1  23076  isnrm3  23083  isreg2  23101  tgcmp  23125  hauscmplem  23130  hauscmp  23131  bwth  23134  1stcfb  23169  1stcelcls  23185  lly1stc  23220  txcmplem1  23365  txlm  23372  xkococnlem  23383  filuni  23609  filufint  23644  ufilen  23654  fclscf  23749  cnextcn  23791  ustex2sym  23941  ustex3sym  23942  utopreg  23977  isucn2  24004  ucnima  24006  ucncn  24010  neipcfilu  24021  metequiv2  24239  metrest  24253  xrsmopn  24548  mulc1cncf  24645  cncfco  24647  bndth  24704  lmmcvg  25009  cfil3i  25017  iscau4  25027  cmetcaulem  25036  iscmet3lem1  25039  caussi  25045  equivcfil  25047  equivcau  25048  caubl  25056  minveclem3b  25176  ovolgelb  25229  ovollb2lem  25237  ovolctb  25239  ovolicc2lem4  25269  ioombl1lem4  25310  dyadmax  25347  volsup2  25354  itg2monolem1  25500  c1liplem1  25748  c1lip1  25749  dvivthlem1  25760  lhop1  25766  ftc1a  25789  ftc1lem6  25793  ply1divex  25889  elply2  25945  dgrlem  25978  aacjcl  26076  aalioulem2  26082  aalioulem3  26083  aalioulem4  26084  ulmcaulem  26142  ulmcau  26143  ulmss  26145  mtest  26152  itgulm  26156  reeff1o  26195  efif1olem4  26290  rlimcnp  26706  xrlimcnp  26709  lgamucov  26778  ftalem3  26815  fta  26820  muval1  26873  dvdssqf  26878  mumullem1  26919  lgsqrmod  27091  lgsqrmodndvds  27092  pntlem3  27348  ostth  27378  nosupno  27442  nosupbnd1lem4  27450  noinfno  27457  noinfbnd1lem4  27465  conway  27537  etasslt  27551  tgtrisegint  28017  tgbtwndiff  28024  tgcgrxfr  28036  lnext  28085  legov2  28104  legtrd  28107  hlcgrex  28134  colperpexlem3  28250  colperpex  28251  hlpasch  28274  hpgerlem  28283  hpgtr  28286  dfcgra2  28348  acopy  28351  inagswap  28359  inaghl  28363  cgrg3col4  28371  axpasch  28466  wwlksnredwwlkn0  29417  midwwlks2s3  29473  clwwlkn1loopb  29563  2pthfrgrrn2  29803  frgrwopreg1  29838  frgrwopreg2  29839  grpoidinvlem3  30026  grpoideu  30029  grpoinveu  30039  ubthlem1  30390  minvecolem5  30401  htthlem  30437  chscllem2  31158  nmopun  31534  lnconi  31553  rnbra  31627  sumdmdii  31935  cdj3lem2b  31957  foresf1o  32009  acunirnmpt  32151  xrofsup  32247  fprodex01  32298  isarchi3  32603  isarchiofld  32705  evls1fpws  32920  lmxrge0  33230  lmdvg  33231  esumlub  33356  esumfsup  33366  esumcvg  33382  ftc2re  33908  cusgr3cyclex  34425  cvmliftmolem2  34571  cvmlift2lem12  34603  satfv1  34652  satffunlem1lem2  34692  satffunlem2lem2  34695  satfv0fvfmla0  34702  wzel  35100  wsuclem  35101  btwndiff  35303  trisegint  35304  cgrxfr  35331  lineext  35352  segcon2  35381  brsegle2  35385  seglecgr12im  35386  segletr  35390  broutsideof3  35402  opnrebl2  35509  nn0prpw  35511  fin2so  36778  poimirlem27  36818  poimirlem30  36821  poimirlem31  36822  poimir  36824  mblfinlem1  36828  mblfinlem2  36829  mblfinlem3  36830  mblfinlem4  36831  itg2addnclem  36842  ftc1cnnc  36863  ftc1anclem5  36868  sdclem1  36914  geomcau  36930  equivtotbnd  36949  bndss  36957  ismtybndlem  36977  heibor1lem  36980  rrncmslem  37003  rngo2  37078  prtlem15  38048  lsateln0  38168  lsat0cv  38206  eqlkr3  38274  lkrshp  38278  lshpset2N  38292  hlhgt2  38563  hlrelat2  38577  atle  38610  athgt  38630  2dim  38644  1cvratex  38647  ps-2  38652  dalem20  38867  lhpexle1lem  39181  lhpexle1  39182  lhpexle2lem  39183  lhpmcvr5N  39201  lhpmcvr6N  39202  cdleme25a  39527  cdleme29ex  39548  cdlemfnid  39738  cdlemg33b0  39875  cdlemg33a  39880  cdlemg35  39887  cdleml3N  40152  dihlsscpre  40408  dih1dimb2  40415  dihatexv  40512  dvh3dim2  40622  dochkr1  40652  dochkr1OLDN  40653  lcfl8  40676  lcfl8b  40678  lcfrlem5  40720  lcfrlem6  40721  mapdrvallem2  40819  mapdh9a  40963  mapdh9aOLDN  40964  hdmaprnlem3eN  41032  hdmaprnlem16N  41036  flt4lem5elem  41695  flt4lem7  41703  nna4b4nsq  41704  fphpdo  41857  rencldnfilem  41860  irrapxlem2  41863  oasubex  42338  tfsconcatlem  42388  tfsconcatrev  42400  cvgdvgrat  43374  expgrowth  43396  projf1o  44194  ssfiunibd  44317  supxrgere  44341  supxrgelem  44345  suplesup  44347  infrpge  44359  infleinf  44380  supxrunb3  44407  unb2ltle  44423  uzub  44439  cvgcaule  44500  qinioo  44546  qelioo  44557  climinf  44620  mullimc  44630  islptre  44633  limccog  44634  mullimcf  44637  limcrecl  44643  sumnnodd  44644  neglimc  44661  0ellimcdiv  44663  limclner  44665  allbutfifvre  44689  climleltrp  44690  fnlimabslt  44693  climinf2lem  44720  limsuppnflem  44724  limsupvaluz2  44752  supcnvlimsup  44754  limsupgtlem  44791  liminflelimsupuz  44799  liminflimsupclim  44821  limsupub2  44826  xlimpnfxnegmnf  44828  cncfioobd  44911  stoweidlem7  45021  stoweidlem27  45041  stoweidlem39  45053  stoweidlem48  45062  stoweidlem49  45063  stoweidlem60  45074  stoweidlem61  45075  stoweid  45077  dirkercncflem2  45118  fourierdlem20  45141  fourierdlem39  45160  fourierdlem41  45162  fourierdlem48  45168  fourierdlem49  45169  fourierdlem50  45170  fourierdlem64  45184  fourierdlem73  45193  fourierdlem74  45194  fourierdlem75  45195  fourierdlem87  45207  fourierdlem103  45223  fourierdlem104  45224  qndenserrnopnlem  45311  sge0ltfirp  45414  sge0gerpmpt  45416  sge0ltfirpmpt2  45440  sge0isum  45441  sge0pnffigtmpt  45454  sge0pnffsumgt  45456  sge0gtfsumgt  45457  sge0uzfsumgt  45458  nnfoctbdjlem  45469  meaiuninclem  45494  meaiuninc3v  45498  omeiunltfirp  45533  carageniuncllem2  45536  hoicvr  45562  volicorescl  45567  hoidmv1le  45608  hoidmvlelem3  45611  hoiqssbllem3  45638  hspmbllem2  45641  iunhoiioolem  45689  vonioo  45696  vonicc  45699  smfaddlem1  45777  smflimlem2  45786  smflimlem3  45787  smfmullem4  45808  fsetsnfo  46061  2reu8i  46119  imasetpreimafvbijlemfo  46371  2pwp1prmfmtno  46556  proththd  46580  sbgoldbwt  46743  sbgoldbst  46744  sbgoldbalt  46747  bgoldbtbndlem4  46774  bgoldbtbnd  46775  zrninitoringc  47057  ply1mulgsumlem3  47156  ply1mulgsumlem4  47157  islindeps2  47251  isldepslvec2  47253