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 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  reximddv  3149  reximdvva  3181  reximddv2  3192  wereu2  5616  frpomin  6292  dffo4  7042  nnaordex  8559  frfi  9176  fisupg  9179  marypha1  9325  fiinfg  9392  wemapsolem  9443  unwdomg  9477  rankr1ai  9698  cofsmo  10167  cfcoflem  10170  inar1  10673  nqerf  10828  prlem936  10945  fimaxre  12073  fiminre  12076  arch  12385  bndndx  12387  suprfinzcl  12593  zmin  12844  elpq  12875  qbtwnxr  13101  qsqueeze  13102  qextltlem  13103  xrsupsslem  13208  xrinfmsslem  13209  xrub  13213  supxrunb1  13220  ssnn0fi  13894  fsuppmapnn0fiub0  13902  fsuppmapnn0fz  13905  expnlbnd2  14143  r19.29uz  15260  cau3lem  15264  rlim2lt  15406  rlimclim  15455  2clim  15481  o1co  15495  climcn1  15501  climcn2  15502  rlimo1  15526  climsqz  15550  climsqz2  15551  rlimsqzlem  15558  lo1le  15561  climsup  15579  climcau  15580  caucvgrlem2  15584  iseralt  15594  cvgcmp  15725  cvgcmpce  15727  supcvg  15765  rpnnen2lem12  16136  bezoutlem1  16452  divgcdcoprmex  16579  exprmfct  16617  prmdvdsfz  16618  prmdvdsncoprmbd  16640  pclem  16752  pc2dvds  16793  pcprmpw  16797  dvdsprmpweqle  16800  unbenlem  16822  infpnlem2  16825  infpn2  16827  prmunb  16828  vdwlem2  16896  ramub1lem2  16941  prmdvdsprmop  16957  prmgaplem7  16971  ipodrsima  18449  smndex1mgm  18817  grpinveu  18889  dfgrp3lem  18953  psgneu  19420  odbezout  19472  sylow2blem3  19536  nn0gsumfz  19898  irredrmul  20347  zrninitoringc  20593  lbsextlem2  21098  znunit  21502  mptcoe1fsupp  22129  evls1fpws  22285  scmate  22426  scmatscm  22429  scmatfo  22446  mat1scmat  22455  pmatcoe1fsupp  22617  pmatcollpwfi  22698  pmatcollpw3fi  22701  mptcoe1matfsupp  22718  pm2mp  22741  chmaidscmat  22764  cpmadumatpoly  22799  chcoeffeq  22802  cayhamlem3  22803  cayhamlem4  22804  neiptopnei  23048  neitr  23096  cnpnei  23180  haust1  23268  isnrm3  23275  isreg2  23293  tgcmp  23317  hauscmplem  23322  hauscmp  23323  bwth  23326  1stcfb  23361  1stcelcls  23377  lly1stc  23412  txcmplem1  23557  txlm  23564  xkococnlem  23575  filuni  23801  filufint  23836  ufilen  23846  fclscf  23941  cnextcn  23983  ustex2sym  24133  ustex3sym  24134  utopreg  24168  isucn2  24194  ucnima  24196  ucncn  24200  neipcfilu  24211  metequiv2  24426  metrest  24440  xrsmopn  24729  mulc1cncf  24826  cncfco  24828  bndth  24885  lmmcvg  25189  cfil3i  25197  iscau4  25207  cmetcaulem  25216  iscmet3lem1  25219  caussi  25225  equivcfil  25227  equivcau  25228  caubl  25236  minveclem3b  25356  ovolgelb  25409  ovollb2lem  25417  ovolctb  25419  ovolicc2lem4  25449  ioombl1lem4  25490  dyadmax  25527  volsup2  25534  itg2monolem1  25679  c1liplem1  25929  c1lip1  25930  dvivthlem1  25941  lhop1  25947  ftc1a  25972  ftc1lem6  25976  ply1divex  26070  elply2  26129  dgrlem  26162  aacjcl  26263  aalioulem2  26269  aalioulem3  26270  aalioulem4  26271  ulmcaulem  26331  ulmcau  26332  ulmss  26334  mtest  26341  itgulm  26345  reeff1o  26385  efif1olem4  26482  rlimcnp  26903  xrlimcnp  26906  lgamucov  26976  ftalem3  27013  fta  27018  muval1  27071  dvdssqf  27076  mumullem1  27117  lgsqrmod  27291  lgsqrmodndvds  27292  pntlem3  27548  ostth  27578  nosupno  27643  nosupbnd1lem4  27651  noinfno  27658  noinfbnd1lem4  27666  conway  27741  etasslt  27755  znegscl  28317  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  28921  wwlksnredwwlkn0  29876  midwwlks2s3  29932  clwwlkn1loopb  30025  2pthfrgrrn2  30265  frgrwopreg1  30300  frgrwopreg2  30301  grpoidinvlem3  30488  grpoideu  30491  grpoinveu  30501  ubthlem1  30852  minvecolem5  30863  htthlem  30899  chscllem2  31620  nmopun  31996  lnconi  32015  rnbra  32089  sumdmdii  32397  cdj3lem2b  32419  foresf1o  32486  acunirnmpt  32643  xrofsup  32754  fprodex01  32813  mndlactfo  33015  mndractfo  33017  isarchi3  33163  isarchiofld  33175  erler  33239  dfufd2lem  33521  constrconj  33779  constrextdg2lem  33782  constrcjcl  33802  lmxrge0  33986  lmdvg  33987  esumlub  34094  esumfsup  34104  esumcvg  34120  ftc2re  34632  cusgr3cyclex  35201  cvmliftmolem2  35347  cvmlift2lem12  35379  satfv1  35428  satffunlem1lem2  35468  satffunlem2lem2  35471  satfv0fvfmla0  35478  ellcsrspsn  35706  r1peuqusdeg1  35708  wzel  35887  wsuclem  35888  btwndiff  36092  trisegint  36093  cgrxfr  36120  lineext  36141  segcon2  36170  brsegle2  36174  seglecgr12im  36175  segletr  36179  broutsideof3  36191  opnrebl2  36386  nn0prpw  36388  fin2so  37668  poimirlem27  37708  poimirlem30  37711  poimirlem31  37712  poimir  37714  mblfinlem1  37718  mblfinlem2  37719  mblfinlem3  37720  mblfinlem4  37721  itg2addnclem  37732  ftc1cnnc  37753  ftc1anclem5  37758  sdclem1  37804  geomcau  37820  equivtotbnd  37839  bndss  37847  ismtybndlem  37867  heibor1lem  37870  rrncmslem  37893  rngo2  37968  prtlem15  38995  lsateln0  39115  lsat0cv  39153  eqlkr3  39221  lkrshp  39225  lshpset2N  39239  hlhgt2  39509  hlrelat2  39523  atle  39556  athgt  39576  2dim  39590  1cvratex  39593  ps-2  39598  dalem20  39813  lhpexle1lem  40127  lhpexle1  40128  lhpexle2lem  40129  lhpmcvr5N  40147  lhpmcvr6N  40148  cdleme25a  40473  cdleme29ex  40494  cdlemfnid  40684  cdlemg33b0  40821  cdlemg33a  40826  cdlemg35  40833  cdleml3N  41098  dihlsscpre  41354  dih1dimb2  41361  dihatexv  41458  dvh3dim2  41568  dochkr1  41598  dochkr1OLDN  41599  lcfl8  41622  lcfl8b  41624  lcfrlem5  41666  lcfrlem6  41667  mapdrvallem2  41765  mapdh9a  41909  mapdh9aOLDN  41910  hdmaprnlem3eN  41978  hdmaprnlem16N  41982  mndmolinv  42209  primrootsunit1  42211  flt4lem5elem  42770  flt4lem7  42778  nna4b4nsq  42779  fphpdo  42935  rencldnfilem  42938  irrapxlem2  42941  oasubex  43404  tfsconcatlem  43454  tfsconcatrev  43466  cvgdvgrat  44431  expgrowth  44453  projf1o  45319  ssfiunibd  45435  supxrgere  45457  supxrgelem  45461  suplesup  45463  infrpge  45475  infleinf  45495  supxrunb3  45522  unb2ltle  45538  uzub  45554  cvgcaule  45614  qinioo  45660  qelioo  45671  climinf  45731  mullimc  45741  islptre  45744  limccog  45745  mullimcf  45748  limcrecl  45754  sumnnodd  45755  neglimc  45770  0ellimcdiv  45772  limclner  45774  allbutfifvre  45798  climleltrp  45799  fnlimabslt  45802  climinf2lem  45829  limsuppnflem  45833  limsupvaluz2  45861  supcnvlimsup  45863  limsupgtlem  45900  liminflelimsupuz  45908  liminflimsupclim  45930  limsupub2  45935  xlimpnfxnegmnf  45937  cncfioobd  46020  stoweidlem7  46130  stoweidlem27  46150  stoweidlem39  46162  stoweidlem48  46171  stoweidlem49  46172  stoweidlem60  46183  stoweidlem61  46184  stoweid  46186  dirkercncflem2  46227  fourierdlem20  46250  fourierdlem39  46269  fourierdlem41  46271  fourierdlem48  46277  fourierdlem49  46278  fourierdlem50  46279  fourierdlem64  46293  fourierdlem73  46302  fourierdlem74  46303  fourierdlem75  46304  fourierdlem87  46316  fourierdlem103  46332  fourierdlem104  46333  qndenserrnopnlem  46420  sge0ltfirp  46523  sge0gerpmpt  46525  sge0ltfirpmpt2  46549  sge0isum  46550  sge0pnffigtmpt  46563  sge0pnffsumgt  46565  sge0gtfsumgt  46566  sge0uzfsumgt  46567  nnfoctbdjlem  46578  meaiuninclem  46603  meaiuninc3v  46607  omeiunltfirp  46642  carageniuncllem2  46645  hoicvr  46671  volicorescl  46676  hoidmv1le  46717  hoidmvlelem3  46720  hoiqssbllem3  46747  hspmbllem2  46750  iunhoiioolem  46798  vonioo  46805  vonicc  46808  smfaddlem1  46886  smflimlem2  46895  smflimlem3  46896  smfmullem4  46917  fsetsnfo  47178  2reu8i  47238  imasetpreimafvbijlemfo  47530  2pwp1prmfmtno  47715  proththd  47739  sbgoldbwt  47902  sbgoldbst  47903  sbgoldbalt  47906  bgoldbtbndlem4  47933  bgoldbtbnd  47934  grtriprop  48066  ply1mulgsumlem3  48514  ply1mulgsumlem4  48515  islindeps2  48609  isldepslvec2  48611