Theorem reximdva 3175

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  reximddv  3178  reximdvva  3210  reximddv2  3221  wereu2  5647  frpomin  6343  dffo4  7103  nnaordex  8650  frfi  9279  fisupg  9282  marypha1  9429  fiinfg  9496  wemapsolem  9547  unwdomg  9581  rankr1ai  9809  cofsmo  10350  cfcoflem  10353  inar1  10863  nqerf  11018  prlem936  11135  fimaxre  12264  fiminre  12267  arch  12606  bndndx  12608  suprfinzcl  12816  zmin  13074  elpq  13106  qbtwnxr  13333  qsqueeze  13334  qextltlem  13335  xrsupsslem  13440  xrinfmsslem  13441  xrub  13445  supxrunb1  13452  ssnn0fi  14131  fsuppmapnn0fiub0  14139  fsuppmapnn0fz  14142  expnlbnd2  14381  r19.29uz  15523  cau3lem  15527  rlim2lt  15669  rlimclim  15718  2clim  15744  o1co  15758  climcn1  15764  climcn2  15765  rlimo1  15789  climsqz  15813  climsqz2  15814  rlimsqzlem  15821  lo1le  15824  climsup  15842  climcau  15843  caucvgrlem2  15847  iseralt  15857  cvgcmp  15988  cvgcmpce  15990  supcvg  16030  rpnnen2lem12  16398  bezoutlem1  16717  divgcdcoprmex  16846  exprmfct  16885  prmdvdsfz  16886  prmdvdsncoprmbd  16908  pclem  17021  pc2dvds  17062  pcprmpw  17066  dvdsprmpweqle  17069  unbenlem  17091  infpnlem2  17094  infpn2  17096  prmunb  17097  vdwlem2  17165  ramub1lem2  17210  prmdvdsprmop  17226  prmgaplem7  17240  ipodrsima  18720  smndex1mgm  19111  grpinveu  19190  dfgrp3lem  19253  psgneu  19725  odbezout  19777  sylow2blem3  19841  nn0gsumfz  20203  irredrmul  20662  zrninitoringc  20933  lbsextlem2  21442  znunit  21874  mptcoe1fsupp  22538  evls1fpws  22692  scmate  22830  scmatscm  22833  scmatfo  22850  mat1scmat  22859  pmatcoe1fsupp  23024  pmatcollpwfi  23105  pmatcollpw3fi  23108  mptcoe1matfsupp  23125  pm2mp  23148  chmaidscmat  23171  cpmadumatpoly  23206  chcoeffeq  23209  cayhamlem3  23210  cayhamlem4  23211  neiptopnei  23455  neitr  23503  cnpnei  23587  haust1  23675  isnrm3  23682  isreg2  23700  tgcmp  23724  hauscmplem  23729  hauscmp  23730  bwth  23733  1stcfb  23768  1stcelcls  23785  lly1stc  23820  txcmplem1  23965  txlm  23972  xkococnlem  23983  filuni  24209  filufint  24244  ufilen  24254  fclscf  24349  cnextcn  24391  ustex2sym  24541  ustex3sym  24542  utopreg  24576  isucn2  24602  ucnima  24604  ucncn  24608  neipcfilu  24619  metequiv2  24834  metrest  24848  xrsmopn  25137  mulc1cncf  25231  cncfco  25233  bndth  25284  lmmcvg  25587  cfil3i  25595  iscau4  25605  cmetcaulem  25614  iscmet3lem1  25617  caussi  25623  equivcfil  25625  equivcau  25626  caubl  25634  minveclem3b  25754  ovolgelb  25806  ovollb2lem  25814  ovolctb  25816  ovolicc2lem4  25846  ioombl1lem4  25887  dyadmax  25924  volsup2  25931  itg2monolem1  26076  c1liplem1  26321  c1lip1  26322  dvivthlem1  26333  lhop1  26339  ftc1a  26362  ftc1lem6  26366  ply1divex  26460  elply2  26519  dgrlem  26553  aacjcl  26659  aalioulem2  26665  aalioulem3  26666  aalioulem4  26667  ulmcaulem  26726  ulmcau  26727  ulmss  26729  mtest  26736  itgulm  26740  reeff1o  26779  efif1olem4  26878  rlimcnp  27298  xrlimcnp  27301  lgamucov  27370  ftalem3  27407  fta  27412  muval1  27465  dvdssqf  27470  mumullem1  27511  lgsqrmod  27684  lgsqrmodndvds  27685  pntlem3  27941  ostth  27971  flt4lem5elem  27986  flt4lem7  27994  nna4b4nsq  27995  fltoprmlem1  27998  nosupno  28065  nosupbnd1lem4  28073  noinfno  28080  noinfbnd1lem4  28088  conway  28170  etaslts  28184  znegscl  28783  tgtrisegint  28967  tgbtwndiff  28974  tgcgrxfr  28986  lnext  29035  legov2  29054  legtrd  29057  hlcgrex  29087  colperpexlem3  29213  colperpex  29214  hlpasch  29239  hpgerlem  29248  hpgtr  29251  dfcgra2  29343  acopy  29346  inagswap  29365  inaghl  29369  cgrg3col4  29377  axpasch  29524  wwlksnredwwlkn0  30490  midwwlks2s3  30546  clwwlkn1loopb  30639  2pthfrgrrn2  30889  frgrwopreg1  30924  frgrwopreg2  30925  grpoidinvlem3  31113  grpoideu  31116  grpoinveu  31126  ubthlem1  31477  minvecolem5  31488  htthlem  31524  chscllem2  32245  nmopun  32621  lnconi  32640  rnbra  32714  sumdmdii  33022  cdj3lem2b  33044  iscgrag  33057  foresf1o  33147  acunirnmpt  33300  xrofsup  33405  fprodex01  33462  mndlactfo  33634  mndractfo  33636  isarchi3  33794  isarchiofld  33806  erler  33872  erld2  33873  dfufd2lem  34127  constrconj  34423  constrextdg2lem  34426  constrcjcl  34446  lmxrge0  34630  lmdvg  34631  esumlub  34738  esumfsup  34748  esumcvg  34764  ftc2re  35273  cusgr3cyclex  35987  cvmliftmolem2  36133  cvmlift2lem12  36165  satfv1  36214  satffunlem1lem2  36254  satffunlem2lem2  36257  satfv0fvfmla0  36264  ellcsrspsn  36492  r1peuqusdeg1  36494  wzel  36678  wsuclem  36679  btwndiff  36884  trisegint  36885  cgrxfr  36912  lineext  36933  segcon2  36962  brsegle2  36966  seglecgr12im  36967  segletr  36971  broutsideof3  36983  opnrebl2  37201  nn0prpw  37203  fin2so  38623  poimirlem27  38658  poimirlem30  38661  poimirlem31  38662  poimir  38664  mblfinlem1  38668  mblfinlem2  38669  mblfinlem3  38670  mblfinlem4  38671  itg2addnclem  38682  ftc1cnnc  38703  ftc1anclem5  38708  sdclem1  38770  geomcau  38786  equivtotbnd  38805  bndss  38813  ismtybndlem  38833  heibor1lem  38836  rrncmslem  38859  rngo2  38934  prtlem15  40025  lsateln0  40145  lsat0cv  40183  eqlkr3  40251  lkrshp  40255  lshpset2N  40269  hlhgt2  40539  hlrelat2  40553  atle  40586  athgt  40606  2dim  40620  1cvratex  40623  ps-2  40628  dalem20  40843  lhpexle1lem  41157  lhpexle1  41158  lhpexle2lem  41159  lhpmcvr5N  41177  lhpmcvr6N  41178  cdleme25a  41503  cdleme29ex  41524  cdlemfnid  41714  cdlemg33b0  41851  cdlemg33a  41856  cdlemg35  41863  cdleml3N  42128  dihlsscpre  42384  dih1dimb2  42391  dihatexv  42488  dvh3dim2  42598  dochkr1  42628  dochkr1OLDN  42629  lcfl8  42652  lcfl8b  42654  lcfrlem5  42696  lcfrlem6  42697  mapdrvallem2  42795  mapdh9a  42939  mapdh9aOLDN  42940  hdmaprnlem3eN  43008  hdmaprnlem16N  43012  mndmolinv  43238  primrootsunit1  43240  fphpdo  43917  rencldnfilem  43920  irrapxlem2  43923  oasubex  44381  tfsconcatlem  44431  tfsconcatrev  44443  cvgdvgrat  45390  expgrowth  45412  projf1o  46304  ssfiunibd  46418  supxrgere  46438  supxrgelem  46442  suplesup  46444  infrpge  46456  infleinf  46476  supxrunb3  46503  unb2ltle  46518  uzub  46534  cvgcaule  46594  qinioo  46640  qelioo  46651  climinf  46711  mullimc  46721  islptre  46724  limccog  46725  mullimcf  46728  limcrecl  46734  sumnnodd  46735  neglimc  46750  0ellimcdiv  46752  limclner  46754  allbutfifvre  46778  climleltrp  46779  fnlimabslt  46782  climinf2lem  46809  limsuppnflem  46813  limsupvaluz2  46841  supcnvlimsup  46843  limsupgtlem  46880  liminflelimsupuz  46888  liminflimsupclim  46910  limsupub2  46915  xlimpnfxnegmnf  46917  cncfioobd  47000  stoweidlem7  47110  stoweidlem27  47130  stoweidlem39  47142  stoweidlem48  47151  stoweidlem49  47152  stoweidlem60  47163  stoweidlem61  47164  stoweid  47166  dirkercncflem2  47207  fourierdlem20  47230  fourierdlem39  47249  fourierdlem41  47251  fourierdlem48  47257  fourierdlem49  47258  fourierdlem50  47259  fourierdlem64  47273  fourierdlem73  47282  fourierdlem74  47283  fourierdlem75  47284  fourierdlem87  47296  fourierdlem103  47312  fourierdlem104  47313  qndenserrnopnlem  47400  sge0ltfirp  47503  sge0gerpmpt  47505  sge0ltfirpmpt2  47529  sge0isum  47530  sge0pnffigtmpt  47543  sge0pnffsumgt  47545  sge0gtfsumgt  47546  sge0uzfsumgt  47547  nnfoctbdjlem  47558  meaiuninclem  47583  meaiuninc3v  47587  omeiunltfirp  47622  carageniuncllem2  47625  volicorescl  47656  hoidmv1le  47697  hoidmvlelem3  47700  hoiqssbllem3  47727  hspmbllem2  47730  iunhoiioolem  47778  vonioo  47785  vonicc  47788  smfaddlem1  47866  smflimlem2  47875  smflimlem3  47876  smfmullem4  47897  fsetsnfo  48216  2reu8i  48276  imasetpreimafvbijlemfo  48580  2pwp1prmfmtno  48768  proththd  48792  sbgoldbwt  48968  sbgoldbst  48969  sbgoldbalt  48972  bgoldbtbndlem4  48999  bgoldbtbnd  49000  grtriprop  49132  ply1mulgsumlem3  49593  ply1mulgsumlem4  49594  islindeps2  49688  isldepslvec2  49690