Theorem reximdva 3146

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  reximddv  3149  reximdvva  3185  reximddv2  3196  wereu2  5635  frpomin  6313  dffo4  7075  nnaordex  8602  frfi  9232  fisupg  9235  marypha1  9385  fiinfg  9452  wemapsolem  9503  unwdomg  9537  rankr1ai  9751  cofsmo  10222  cfcoflem  10225  inar1  10728  nqerf  10883  prlem936  11000  fimaxre  12127  fiminre  12130  arch  12439  bndndx  12441  suprfinzcl  12648  zmin  12903  elpq  12934  qbtwnxr  13160  qsqueeze  13161  qextltlem  13162  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  supxrunb1  13279  ssnn0fi  13950  fsuppmapnn0fiub0  13958  fsuppmapnn0fz  13961  expnlbnd2  14199  r19.29uz  15317  cau3lem  15321  rlim2lt  15463  rlimclim  15512  2clim  15538  o1co  15552  climcn1  15558  climcn2  15559  rlimo1  15583  climsqz  15607  climsqz2  15608  rlimsqzlem  15615  lo1le  15618  climsup  15636  climcau  15637  caucvgrlem2  15641  iseralt  15651  cvgcmp  15782  cvgcmpce  15784  supcvg  15822  rpnnen2lem12  16193  bezoutlem1  16509  divgcdcoprmex  16636  exprmfct  16674  prmdvdsfz  16675  prmdvdsncoprmbd  16697  pclem  16809  pc2dvds  16850  pcprmpw  16854  dvdsprmpweqle  16857  unbenlem  16879  infpnlem2  16882  infpn2  16884  prmunb  16885  vdwlem2  16953  ramub1lem2  16998  prmdvdsprmop  17014  prmgaplem7  17028  ipodrsima  18500  smndex1mgm  18834  grpinveu  18906  dfgrp3lem  18970  psgneu  19436  odbezout  19488  sylow2blem3  19552  nn0gsumfz  19914  irredrmul  20336  zrninitoringc  20585  lbsextlem2  21069  znunit  21473  mptcoe1fsupp  22100  evls1fpws  22256  scmate  22397  scmatscm  22400  scmatfo  22417  mat1scmat  22426  pmatcoe1fsupp  22588  pmatcollpwfi  22669  pmatcollpw3fi  22672  mptcoe1matfsupp  22689  pm2mp  22712  chmaidscmat  22735  cpmadumatpoly  22770  chcoeffeq  22773  cayhamlem3  22774  cayhamlem4  22775  neiptopnei  23019  neitr  23067  cnpnei  23151  haust1  23239  isnrm3  23246  isreg2  23264  tgcmp  23288  hauscmplem  23293  hauscmp  23294  bwth  23297  1stcfb  23332  1stcelcls  23348  lly1stc  23383  txcmplem1  23528  txlm  23535  xkococnlem  23546  filuni  23772  filufint  23807  ufilen  23817  fclscf  23912  cnextcn  23954  ustex2sym  24104  ustex3sym  24105  utopreg  24140  isucn2  24166  ucnima  24168  ucncn  24172  neipcfilu  24183  metequiv2  24398  metrest  24412  xrsmopn  24701  mulc1cncf  24798  cncfco  24800  bndth  24857  lmmcvg  25161  cfil3i  25169  iscau4  25179  cmetcaulem  25188  iscmet3lem1  25191  caussi  25197  equivcfil  25199  equivcau  25200  caubl  25208  minveclem3b  25328  ovolgelb  25381  ovollb2lem  25389  ovolctb  25391  ovolicc2lem4  25421  ioombl1lem4  25462  dyadmax  25499  volsup2  25506  itg2monolem1  25651  c1liplem1  25901  c1lip1  25902  dvivthlem1  25913  lhop1  25919  ftc1a  25944  ftc1lem6  25948  ply1divex  26042  elply2  26101  dgrlem  26134  aacjcl  26235  aalioulem2  26241  aalioulem3  26242  aalioulem4  26243  ulmcaulem  26303  ulmcau  26304  ulmss  26306  mtest  26313  itgulm  26317  reeff1o  26357  efif1olem4  26454  rlimcnp  26875  xrlimcnp  26878  lgamucov  26948  ftalem3  26985  fta  26990  muval1  27043  dvdssqf  27048  mumullem1  27089  lgsqrmod  27263  lgsqrmodndvds  27264  pntlem3  27520  ostth  27550  nosupno  27615  nosupbnd1lem4  27623  noinfno  27630  noinfbnd1lem4  27638  conway  27711  etasslt  27725  znegscl  28280  tgtrisegint  28426  tgbtwndiff  28433  tgcgrxfr  28445  lnext  28494  legov2  28513  legtrd  28516  hlcgrex  28543  colperpexlem3  28659  colperpex  28660  hlpasch  28683  hpgerlem  28692  hpgtr  28695  dfcgra2  28757  acopy  28760  inagswap  28768  inaghl  28772  cgrg3col4  28780  axpasch  28868  wwlksnredwwlkn0  29826  midwwlks2s3  29882  clwwlkn1loopb  29972  2pthfrgrrn2  30212  frgrwopreg1  30247  frgrwopreg2  30248  grpoidinvlem3  30435  grpoideu  30438  grpoinveu  30448  ubthlem1  30799  minvecolem5  30810  htthlem  30846  chscllem2  31567  nmopun  31943  lnconi  31962  rnbra  32036  sumdmdii  32344  cdj3lem2b  32366  foresf1o  32433  acunirnmpt  32583  xrofsup  32690  fprodex01  32750  mndlactfo  32968  mndractfo  32970  isarchi3  33141  erler  33216  isarchiofld  33295  dfufd2lem  33520  constrconj  33735  constrextdg2lem  33738  constrcjcl  33758  lmxrge0  33942  lmdvg  33943  esumlub  34050  esumfsup  34060  esumcvg  34076  ftc2re  34589  cusgr3cyclex  35123  cvmliftmolem2  35269  cvmlift2lem12  35301  satfv1  35350  satffunlem1lem2  35390  satffunlem2lem2  35393  satfv0fvfmla0  35400  ellcsrspsn  35628  r1peuqusdeg1  35630  wzel  35812  wsuclem  35813  btwndiff  36015  trisegint  36016  cgrxfr  36043  lineext  36064  segcon2  36093  brsegle2  36097  seglecgr12im  36098  segletr  36102  broutsideof3  36114  opnrebl2  36309  nn0prpw  36311  fin2so  37601  poimirlem27  37641  poimirlem30  37644  poimirlem31  37645  poimir  37647  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem  37665  ftc1cnnc  37686  ftc1anclem5  37691  sdclem1  37737  geomcau  37753  equivtotbnd  37772  bndss  37780  ismtybndlem  37800  heibor1lem  37803  rrncmslem  37826  rngo2  37901  prtlem15  38868  lsateln0  38988  lsat0cv  39026  eqlkr3  39094  lkrshp  39098  lshpset2N  39112  hlhgt2  39383  hlrelat2  39397  atle  39430  athgt  39450  2dim  39464  1cvratex  39467  ps-2  39472  dalem20  39687  lhpexle1lem  40001  lhpexle1  40002  lhpexle2lem  40003  lhpmcvr5N  40021  lhpmcvr6N  40022  cdleme25a  40347  cdleme29ex  40368  cdlemfnid  40558  cdlemg33b0  40695  cdlemg33a  40700  cdlemg35  40707  cdleml3N  40972  dihlsscpre  41228  dih1dimb2  41235  dihatexv  41332  dvh3dim2  41442  dochkr1  41472  dochkr1OLDN  41473  lcfl8  41496  lcfl8b  41498  lcfrlem5  41540  lcfrlem6  41541  mapdrvallem2  41639  mapdh9a  41783  mapdh9aOLDN  41784  hdmaprnlem3eN  41852  hdmaprnlem16N  41856  mndmolinv  42083  primrootsunit1  42085  flt4lem5elem  42639  flt4lem7  42647  nna4b4nsq  42648  fphpdo  42805  rencldnfilem  42808  irrapxlem2  42811  oasubex  43275  tfsconcatlem  43325  tfsconcatrev  43337  cvgdvgrat  44302  expgrowth  44324  projf1o  45191  ssfiunibd  45307  supxrgere  45329  supxrgelem  45333  suplesup  45335  infrpge  45347  infleinf  45368  supxrunb3  45395  unb2ltle  45411  uzub  45427  cvgcaule  45487  qinioo  45533  qelioo  45544  climinf  45604  mullimc  45614  islptre  45617  limccog  45618  mullimcf  45621  limcrecl  45627  sumnnodd  45628  neglimc  45645  0ellimcdiv  45647  limclner  45649  allbutfifvre  45673  climleltrp  45674  fnlimabslt  45677  climinf2lem  45704  limsuppnflem  45708  limsupvaluz2  45736  supcnvlimsup  45738  limsupgtlem  45775  liminflelimsupuz  45783  liminflimsupclim  45805  limsupub2  45810  xlimpnfxnegmnf  45812  cncfioobd  45895  stoweidlem7  46005  stoweidlem27  46025  stoweidlem39  46037  stoweidlem48  46046  stoweidlem49  46047  stoweidlem60  46058  stoweidlem61  46059  stoweid  46061  dirkercncflem2  46102  fourierdlem20  46125  fourierdlem39  46144  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem64  46168  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  qndenserrnopnlem  46295  sge0ltfirp  46398  sge0gerpmpt  46400  sge0ltfirpmpt2  46424  sge0isum  46425  sge0pnffigtmpt  46438  sge0pnffsumgt  46440  sge0gtfsumgt  46441  sge0uzfsumgt  46442  nnfoctbdjlem  46453  meaiuninclem  46478  meaiuninc3v  46482  omeiunltfirp  46517  carageniuncllem2  46520  hoicvr  46546  volicorescl  46551  hoidmv1le  46592  hoidmvlelem3  46595  hoiqssbllem3  46622  hspmbllem2  46625  iunhoiioolem  46673  vonioo  46680  vonicc  46683  smfaddlem1  46761  smflimlem2  46770  smflimlem3  46771  smfmullem4  46792  fsetsnfo  47054  2reu8i  47114  imasetpreimafvbijlemfo  47406  2pwp1prmfmtno  47591  proththd  47615  sbgoldbwt  47778  sbgoldbst  47779  sbgoldbalt  47782  bgoldbtbndlem4  47809  bgoldbtbnd  47810  grtriprop  47940  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378  islindeps2  48472  isldepslvec2  48474