Theorem reximdva 3161

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3069

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3070

This theorem is referenced by:  reximddv  3164  reximdvva  3198  reximddv2  3202  wereu2  5635  frpomin  6299  dffo4  7058  nnaordex  8590  frfi  9239  fisupg  9242  marypha1  9379  fiinfg  9444  wemapsolem  9495  unwdomg  9529  rankr1ai  9743  cofsmo  10214  cfcoflem  10217  inar1  10720  nqerf  10875  prlem936  10992  fimaxre  12108  fiminre  12111  arch  12419  bndndx  12421  suprfinzcl  12626  zmin  12878  elpq  12909  qbtwnxr  13129  qsqueeze  13130  qextltlem  13131  xrsupsslem  13236  xrinfmsslem  13237  xrub  13241  supxrunb1  13248  ssnn0fi  13900  fsuppmapnn0fiub0  13908  fsuppmapnn0fz  13911  expnlbnd2  14147  r19.29uz  15247  cau3lem  15251  rlim2lt  15391  rlimclim  15440  2clim  15466  o1co  15480  climcn1  15486  climcn2  15487  rlimo1  15511  climsqz  15535  climsqz2  15536  rlimsqzlem  15545  lo1le  15548  climsup  15566  climcau  15567  caucvgrlem2  15571  iseralt  15581  cvgcmp  15712  cvgcmpce  15714  supcvg  15752  rpnnen2lem12  16118  bezoutlem1  16431  divgcdcoprmex  16553  exprmfct  16591  prmdvdsfz  16592  prmdvdsncoprmbd  16613  pclem  16721  pc2dvds  16762  pcprmpw  16766  dvdsprmpweqle  16769  unbenlem  16791  infpnlem2  16794  infpn2  16796  prmunb  16797  vdwlem2  16865  ramub1lem2  16910  prmdvdsprmop  16926  prmgaplem7  16940  ipodrsima  18444  smndex1mgm  18731  grpinveu  18799  dfgrp3lem  18859  psgneu  19302  odbezout  19354  sylow2blem3  19418  nn0gsumfz  19775  irredrmul  20152  lbsextlem2  20679  znunit  21007  mptcoe1fsupp  21623  scmate  21896  scmatscm  21899  scmatfo  21916  mat1scmat  21925  pmatcoe1fsupp  22087  pmatcollpwfi  22168  pmatcollpw3fi  22171  mptcoe1matfsupp  22188  pm2mp  22211  chmaidscmat  22234  cpmadumatpoly  22269  chcoeffeq  22272  cayhamlem3  22273  cayhamlem4  22274  neiptopnei  22520  neitr  22568  cnpnei  22652  haust1  22740  isnrm3  22747  isreg2  22765  tgcmp  22789  hauscmplem  22794  hauscmp  22795  bwth  22798  1stcfb  22833  1stcelcls  22849  lly1stc  22884  txcmplem1  23029  txlm  23036  xkococnlem  23047  filuni  23273  filufint  23308  ufilen  23318  fclscf  23413  cnextcn  23455  ustex2sym  23605  ustex3sym  23606  utopreg  23641  isucn2  23668  ucnima  23670  ucncn  23674  neipcfilu  23685  metequiv2  23903  metrest  23917  xrsmopn  24212  mulc1cncf  24305  cncfco  24307  bndth  24358  lmmcvg  24662  cfil3i  24670  iscau4  24680  cmetcaulem  24689  iscmet3lem1  24692  caussi  24698  equivcfil  24700  equivcau  24701  caubl  24709  minveclem3b  24829  ovolgelb  24881  ovollb2lem  24889  ovolctb  24891  ovolicc2lem4  24921  ioombl1lem4  24962  dyadmax  24999  volsup2  25006  itg2monolem1  25152  c1liplem1  25397  c1lip1  25398  dvivthlem1  25409  lhop1  25415  ftc1a  25438  ftc1lem6  25442  ply1divex  25538  elply2  25594  dgrlem  25627  aacjcl  25724  aalioulem2  25730  aalioulem3  25731  aalioulem4  25732  ulmcaulem  25790  ulmcau  25791  ulmss  25793  mtest  25800  itgulm  25804  reeff1o  25843  efif1olem4  25938  rlimcnp  26352  xrlimcnp  26355  lgamucov  26424  ftalem3  26461  fta  26466  muval1  26519  dvdssqf  26524  mumullem1  26565  lgsqrmod  26737  lgsqrmodndvds  26738  pntlem3  26994  ostth  27024  nosupno  27088  nosupbnd1lem4  27096  noinfno  27103  noinfbnd1lem4  27111  conway  27181  etasslt  27195  tgtrisegint  27504  tgbtwndiff  27511  tgcgrxfr  27523  lnext  27572  legov2  27591  legtrd  27594  hlcgrex  27621  colperpexlem3  27737  colperpex  27738  hlpasch  27761  hpgerlem  27770  hpgtr  27773  dfcgra2  27835  acopy  27838  inagswap  27846  inaghl  27850  cgrg3col4  27858  axpasch  27953  wwlksnredwwlkn0  28904  midwwlks2s3  28960  clwwlkn1loopb  29050  2pthfrgrrn2  29290  frgrwopreg1  29325  frgrwopreg2  29326  grpoidinvlem3  29511  grpoideu  29514  grpoinveu  29524  ubthlem1  29875  minvecolem5  29886  htthlem  29922  chscllem2  30643  nmopun  31019  lnconi  31038  rnbra  31112  sumdmdii  31420  cdj3lem2b  31442  foresf1o  31495  acunirnmpt  31642  xrofsup  31740  fprodex01  31791  isarchi3  32093  isarchiofld  32183  evls1fpws  32348  lmxrge0  32622  lmdvg  32623  esumlub  32748  esumfsup  32758  esumcvg  32774  ftc2re  33300  cusgr3cyclex  33817  cvmliftmolem2  33963  cvmlift2lem12  33995  satfv1  34044  satffunlem1lem2  34084  satffunlem2lem2  34087  satfv0fvfmla0  34094  wzel  34485  wsuclem  34486  btwndiff  34688  trisegint  34689  cgrxfr  34716  lineext  34737  segcon2  34766  brsegle2  34770  seglecgr12im  34771  segletr  34775  broutsideof3  34787  opnrebl2  34869  nn0prpw  34871  fin2so  36138  poimirlem27  36178  poimirlem30  36181  poimirlem31  36182  poimir  36184  mblfinlem1  36188  mblfinlem2  36189  mblfinlem3  36190  mblfinlem4  36191  itg2addnclem  36202  ftc1cnnc  36223  ftc1anclem5  36228  sdclem1  36275  geomcau  36291  equivtotbnd  36310  bndss  36318  ismtybndlem  36338  heibor1lem  36341  rrncmslem  36364  rngo2  36439  prtlem15  37410  lsateln0  37530  lsat0cv  37568  eqlkr3  37636  lkrshp  37640  lshpset2N  37654  hlhgt2  37925  hlrelat2  37939  atle  37972  athgt  37992  2dim  38006  1cvratex  38009  ps-2  38014  dalem20  38229  lhpexle1lem  38543  lhpexle1  38544  lhpexle2lem  38545  lhpmcvr5N  38563  lhpmcvr6N  38564  cdleme25a  38889  cdleme29ex  38910  cdlemfnid  39100  cdlemg33b0  39237  cdlemg33a  39242  cdlemg35  39249  cdleml3N  39514  dihlsscpre  39770  dih1dimb2  39777  dihatexv  39874  dvh3dim2  39984  dochkr1  40014  dochkr1OLDN  40015  lcfl8  40038  lcfl8b  40040  lcfrlem5  40082  lcfrlem6  40083  mapdrvallem2  40181  mapdh9a  40325  mapdh9aOLDN  40326  hdmaprnlem3eN  40394  hdmaprnlem16N  40398  flt4lem5elem  41047  flt4lem7  41055  nna4b4nsq  41056  fphpdo  41198  rencldnfilem  41201  irrapxlem2  41204  oasubex  41679  tfsconcatlem  41729  tfsconcatrev  41741  cvgdvgrat  42715  expgrowth  42737  projf1o  43539  ssfiunibd  43664  supxrgere  43688  supxrgelem  43692  suplesup  43694  infrpge  43706  infleinf  43727  supxrunb3  43754  unb2ltle  43770  uzub  43786  cvgcaule  43847  qinioo  43893  qelioo  43904  climinf  43967  mullimc  43977  islptre  43980  limccog  43981  mullimcf  43984  limcrecl  43990  sumnnodd  43991  neglimc  44008  0ellimcdiv  44010  limclner  44012  allbutfifvre  44036  climleltrp  44037  fnlimabslt  44040  climinf2lem  44067  limsuppnflem  44071  limsupvaluz2  44099  supcnvlimsup  44101  limsupgtlem  44138  liminflelimsupuz  44146  liminflimsupclim  44168  limsupub2  44173  xlimpnfxnegmnf  44175  cncfioobd  44258  stoweidlem7  44368  stoweidlem27  44388  stoweidlem39  44400  stoweidlem48  44409  stoweidlem49  44410  stoweidlem60  44421  stoweidlem61  44422  stoweid  44424  dirkercncflem2  44465  fourierdlem20  44488  fourierdlem39  44507  fourierdlem41  44509  fourierdlem48  44515  fourierdlem49  44516  fourierdlem50  44517  fourierdlem64  44531  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem87  44554  fourierdlem103  44570  fourierdlem104  44571  qndenserrnopnlem  44658  sge0ltfirp  44761  sge0gerpmpt  44763  sge0ltfirpmpt2  44787  sge0isum  44788  sge0pnffigtmpt  44801  sge0pnffsumgt  44803  sge0gtfsumgt  44804  sge0uzfsumgt  44805  nnfoctbdjlem  44816  meaiuninclem  44841  meaiuninc3v  44845  omeiunltfirp  44880  carageniuncllem2  44883  hoicvr  44909  volicorescl  44914  hoidmv1le  44955  hoidmvlelem3  44958  hoiqssbllem3  44985  hspmbllem2  44988  iunhoiioolem  45036  vonioo  45043  vonicc  45046  smfaddlem1  45124  smflimlem2  45133  smflimlem3  45134  smfmullem4  45155  fsetsnfo  45407  2reu8i  45465  imasetpreimafvbijlemfo  45717  2pwp1prmfmtno  45902  proththd  45926  sbgoldbwt  46089  sbgoldbst  46090  sbgoldbalt  46093  bgoldbtbndlem4  46120  bgoldbtbnd  46121  zrninitoringc  46489  ply1mulgsumlem3  46589  ply1mulgsumlem4  46590  islindeps2  46684  isldepslvec2  46686