Theorem reximdva 3153

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

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

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 3061

This theorem is referenced by:  reximddv  3156  reximdvva  3192  reximddv2  3200  wereu2  5651  frpomin  6329  dffo4  7093  nnaordex  8650  frfi  9293  fisupg  9296  marypha1  9446  fiinfg  9513  wemapsolem  9564  unwdomg  9598  rankr1ai  9812  cofsmo  10283  cfcoflem  10286  inar1  10789  nqerf  10944  prlem936  11061  fimaxre  12186  fiminre  12189  arch  12498  bndndx  12500  suprfinzcl  12707  zmin  12960  elpq  12991  qbtwnxr  13216  qsqueeze  13217  qextltlem  13218  xrsupsslem  13323  xrinfmsslem  13324  xrub  13328  supxrunb1  13335  ssnn0fi  14003  fsuppmapnn0fiub0  14011  fsuppmapnn0fz  14014  expnlbnd2  14252  r19.29uz  15369  cau3lem  15373  rlim2lt  15513  rlimclim  15562  2clim  15588  o1co  15602  climcn1  15608  climcn2  15609  rlimo1  15633  climsqz  15657  climsqz2  15658  rlimsqzlem  15665  lo1le  15668  climsup  15686  climcau  15687  caucvgrlem2  15691  iseralt  15701  cvgcmp  15832  cvgcmpce  15834  supcvg  15872  rpnnen2lem12  16243  bezoutlem1  16558  divgcdcoprmex  16685  exprmfct  16723  prmdvdsfz  16724  prmdvdsncoprmbd  16746  pclem  16858  pc2dvds  16899  pcprmpw  16903  dvdsprmpweqle  16906  unbenlem  16928  infpnlem2  16931  infpn2  16933  prmunb  16934  vdwlem2  17002  ramub1lem2  17047  prmdvdsprmop  17063  prmgaplem7  17077  ipodrsima  18551  smndex1mgm  18885  grpinveu  18957  dfgrp3lem  19021  psgneu  19487  odbezout  19539  sylow2blem3  19603  nn0gsumfz  19965  irredrmul  20387  zrninitoringc  20636  lbsextlem2  21120  znunit  21524  mptcoe1fsupp  22151  evls1fpws  22307  scmate  22448  scmatscm  22451  scmatfo  22468  mat1scmat  22477  pmatcoe1fsupp  22639  pmatcollpwfi  22720  pmatcollpw3fi  22723  mptcoe1matfsupp  22740  pm2mp  22763  chmaidscmat  22786  cpmadumatpoly  22821  chcoeffeq  22824  cayhamlem3  22825  cayhamlem4  22826  neiptopnei  23070  neitr  23118  cnpnei  23202  haust1  23290  isnrm3  23297  isreg2  23315  tgcmp  23339  hauscmplem  23344  hauscmp  23345  bwth  23348  1stcfb  23383  1stcelcls  23399  lly1stc  23434  txcmplem1  23579  txlm  23586  xkococnlem  23597  filuni  23823  filufint  23858  ufilen  23868  fclscf  23963  cnextcn  24005  ustex2sym  24155  ustex3sym  24156  utopreg  24191  isucn2  24217  ucnima  24219  ucncn  24223  neipcfilu  24234  metequiv2  24449  metrest  24463  xrsmopn  24752  mulc1cncf  24849  cncfco  24851  bndth  24908  lmmcvg  25213  cfil3i  25221  iscau4  25231  cmetcaulem  25240  iscmet3lem1  25243  caussi  25249  equivcfil  25251  equivcau  25252  caubl  25260  minveclem3b  25380  ovolgelb  25433  ovollb2lem  25441  ovolctb  25443  ovolicc2lem4  25473  ioombl1lem4  25514  dyadmax  25551  volsup2  25558  itg2monolem1  25703  c1liplem1  25953  c1lip1  25954  dvivthlem1  25965  lhop1  25971  ftc1a  25996  ftc1lem6  26000  ply1divex  26094  elply2  26153  dgrlem  26186  aacjcl  26287  aalioulem2  26293  aalioulem3  26294  aalioulem4  26295  ulmcaulem  26355  ulmcau  26356  ulmss  26358  mtest  26365  itgulm  26369  reeff1o  26409  efif1olem4  26506  rlimcnp  26927  xrlimcnp  26930  lgamucov  27000  ftalem3  27037  fta  27042  muval1  27095  dvdssqf  27100  mumullem1  27141  lgsqrmod  27315  lgsqrmodndvds  27316  pntlem3  27572  ostth  27602  nosupno  27667  nosupbnd1lem4  27675  noinfno  27682  noinfbnd1lem4  27690  conway  27763  etasslt  27777  znegscl  28332  tgtrisegint  28478  tgbtwndiff  28485  tgcgrxfr  28497  lnext  28546  legov2  28565  legtrd  28568  hlcgrex  28595  colperpexlem3  28711  colperpex  28712  hlpasch  28735  hpgerlem  28744  hpgtr  28747  dfcgra2  28809  acopy  28812  inagswap  28820  inaghl  28824  cgrg3col4  28832  axpasch  28920  wwlksnredwwlkn0  29878  midwwlks2s3  29934  clwwlkn1loopb  30024  2pthfrgrrn2  30264  frgrwopreg1  30299  frgrwopreg2  30300  grpoidinvlem3  30487  grpoideu  30490  grpoinveu  30500  ubthlem1  30851  minvecolem5  30862  htthlem  30898  chscllem2  31619  nmopun  31995  lnconi  32014  rnbra  32088  sumdmdii  32396  cdj3lem2b  32418  foresf1o  32485  acunirnmpt  32637  xrofsup  32744  fprodex01  32804  mndlactfo  33022  mndractfo  33024  isarchi3  33185  erler  33260  isarchiofld  33339  dfufd2lem  33564  constrconj  33779  constrextdg2lem  33782  constrcjcl  33802  lmxrge0  33983  lmdvg  33984  esumlub  34091  esumfsup  34101  esumcvg  34117  ftc2re  34630  cusgr3cyclex  35158  cvmliftmolem2  35304  cvmlift2lem12  35336  satfv1  35385  satffunlem1lem2  35425  satffunlem2lem2  35428  satfv0fvfmla0  35435  ellcsrspsn  35663  r1peuqusdeg1  35665  wzel  35842  wsuclem  35843  btwndiff  36045  trisegint  36046  cgrxfr  36073  lineext  36094  segcon2  36123  brsegle2  36127  seglecgr12im  36128  segletr  36132  broutsideof3  36144  opnrebl2  36339  nn0prpw  36341  fin2so  37631  poimirlem27  37671  poimirlem30  37674  poimirlem31  37675  poimir  37677  mblfinlem1  37681  mblfinlem2  37682  mblfinlem3  37683  mblfinlem4  37684  itg2addnclem  37695  ftc1cnnc  37716  ftc1anclem5  37721  sdclem1  37767  geomcau  37783  equivtotbnd  37802  bndss  37810  ismtybndlem  37830  heibor1lem  37833  rrncmslem  37856  rngo2  37931  prtlem15  38893  lsateln0  39013  lsat0cv  39051  eqlkr3  39119  lkrshp  39123  lshpset2N  39137  hlhgt2  39408  hlrelat2  39422  atle  39455  athgt  39475  2dim  39489  1cvratex  39492  ps-2  39497  dalem20  39712  lhpexle1lem  40026  lhpexle1  40027  lhpexle2lem  40028  lhpmcvr5N  40046  lhpmcvr6N  40047  cdleme25a  40372  cdleme29ex  40393  cdlemfnid  40583  cdlemg33b0  40720  cdlemg33a  40725  cdlemg35  40732  cdleml3N  40997  dihlsscpre  41253  dih1dimb2  41260  dihatexv  41357  dvh3dim2  41467  dochkr1  41497  dochkr1OLDN  41498  lcfl8  41521  lcfl8b  41523  lcfrlem5  41565  lcfrlem6  41566  mapdrvallem2  41664  mapdh9a  41808  mapdh9aOLDN  41809  hdmaprnlem3eN  41877  hdmaprnlem16N  41881  mndmolinv  42108  primrootsunit1  42110  flt4lem5elem  42674  flt4lem7  42682  nna4b4nsq  42683  fphpdo  42840  rencldnfilem  42843  irrapxlem2  42846  oasubex  43310  tfsconcatlem  43360  tfsconcatrev  43372  cvgdvgrat  44337  expgrowth  44359  projf1o  45221  ssfiunibd  45338  supxrgere  45360  supxrgelem  45364  suplesup  45366  infrpge  45378  infleinf  45399  supxrunb3  45426  unb2ltle  45442  uzub  45458  cvgcaule  45518  qinioo  45564  qelioo  45575  climinf  45635  mullimc  45645  islptre  45648  limccog  45649  mullimcf  45652  limcrecl  45658  sumnnodd  45659  neglimc  45676  0ellimcdiv  45678  limclner  45680  allbutfifvre  45704  climleltrp  45705  fnlimabslt  45708  climinf2lem  45735  limsuppnflem  45739  limsupvaluz2  45767  supcnvlimsup  45769  limsupgtlem  45806  liminflelimsupuz  45814  liminflimsupclim  45836  limsupub2  45841  xlimpnfxnegmnf  45843  cncfioobd  45926  stoweidlem7  46036  stoweidlem27  46056  stoweidlem39  46068  stoweidlem48  46077  stoweidlem49  46078  stoweidlem60  46089  stoweidlem61  46090  stoweid  46092  dirkercncflem2  46133  fourierdlem20  46156  fourierdlem39  46175  fourierdlem41  46177  fourierdlem48  46183  fourierdlem49  46184  fourierdlem50  46185  fourierdlem64  46199  fourierdlem73  46208  fourierdlem74  46209  fourierdlem75  46210  fourierdlem87  46222  fourierdlem103  46238  fourierdlem104  46239  qndenserrnopnlem  46326  sge0ltfirp  46429  sge0gerpmpt  46431  sge0ltfirpmpt2  46455  sge0isum  46456  sge0pnffigtmpt  46469  sge0pnffsumgt  46471  sge0gtfsumgt  46472  sge0uzfsumgt  46473  nnfoctbdjlem  46484  meaiuninclem  46509  meaiuninc3v  46513  omeiunltfirp  46548  carageniuncllem2  46551  hoicvr  46577  volicorescl  46582  hoidmv1le  46623  hoidmvlelem3  46626  hoiqssbllem3  46653  hspmbllem2  46656  iunhoiioolem  46704  vonioo  46711  vonicc  46714  smfaddlem1  46792  smflimlem2  46801  smflimlem3  46802  smfmullem4  46823  fsetsnfo  47082  2reu8i  47142  imasetpreimafvbijlemfo  47419  2pwp1prmfmtno  47604  proththd  47628  sbgoldbwt  47791  sbgoldbst  47792  sbgoldbalt  47795  bgoldbtbndlem4  47822  bgoldbtbnd  47823  grtriprop  47953  ply1mulgsumlem3  48364  ply1mulgsumlem4  48365  islindeps2  48459  isldepslvec2  48461