Theorem reximdva 3145

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  reximddv  3148  reximdvva  3180  reximddv2  3191  wereu2  5613  frpomin  6287  dffo4  7036  nnaordex  8553  frfi  9169  fisupg  9172  marypha1  9318  fiinfg  9385  wemapsolem  9436  unwdomg  9470  rankr1ai  9691  cofsmo  10160  cfcoflem  10163  inar1  10666  nqerf  10821  prlem936  10938  fimaxre  12066  fiminre  12069  arch  12378  bndndx  12380  suprfinzcl  12587  zmin  12842  elpq  12873  qbtwnxr  13099  qsqueeze  13100  qextltlem  13101  xrsupsslem  13206  xrinfmsslem  13207  xrub  13211  supxrunb1  13218  ssnn0fi  13892  fsuppmapnn0fiub0  13900  fsuppmapnn0fz  13903  expnlbnd2  14141  r19.29uz  15258  cau3lem  15262  rlim2lt  15404  rlimclim  15453  2clim  15479  o1co  15493  climcn1  15499  climcn2  15500  rlimo1  15524  climsqz  15548  climsqz2  15549  rlimsqzlem  15556  lo1le  15559  climsup  15577  climcau  15578  caucvgrlem2  15582  iseralt  15592  cvgcmp  15723  cvgcmpce  15725  supcvg  15763  rpnnen2lem12  16134  bezoutlem1  16450  divgcdcoprmex  16577  exprmfct  16615  prmdvdsfz  16616  prmdvdsncoprmbd  16638  pclem  16750  pc2dvds  16791  pcprmpw  16795  dvdsprmpweqle  16798  unbenlem  16820  infpnlem2  16823  infpn2  16825  prmunb  16826  vdwlem2  16894  ramub1lem2  16939  prmdvdsprmop  16955  prmgaplem7  16969  ipodrsima  18447  smndex1mgm  18815  grpinveu  18887  dfgrp3lem  18951  psgneu  19419  odbezout  19471  sylow2blem3  19535  nn0gsumfz  19897  irredrmul  20346  zrninitoringc  20592  lbsextlem2  21097  znunit  21501  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  28920  wwlksnredwwlkn0  29875  midwwlks2s3  29931  clwwlkn1loopb  30021  2pthfrgrrn2  30261  frgrwopreg1  30296  frgrwopreg2  30297  grpoidinvlem3  30484  grpoideu  30487  grpoinveu  30497  ubthlem1  30848  minvecolem5  30859  htthlem  30895  chscllem2  31616  nmopun  31992  lnconi  32011  rnbra  32085  sumdmdii  32393  cdj3lem2b  32415  foresf1o  32482  acunirnmpt  32639  xrofsup  32748  fprodex01  32806  mndlactfo  33006  mndractfo  33008  isarchi3  33154  isarchiofld  33166  erler  33230  dfufd2lem  33512  constrconj  33756  constrextdg2lem  33759  constrcjcl  33779  lmxrge0  33963  lmdvg  33964  esumlub  34071  esumfsup  34081  esumcvg  34097  ftc2re  34609  cusgr3cyclex  35178  cvmliftmolem2  35324  cvmlift2lem12  35356  satfv1  35405  satffunlem1lem2  35445  satffunlem2lem2  35448  satfv0fvfmla0  35455  ellcsrspsn  35683  r1peuqusdeg1  35685  wzel  35864  wsuclem  35865  btwndiff  36067  trisegint  36068  cgrxfr  36095  lineext  36116  segcon2  36145  brsegle2  36149  seglecgr12im  36150  segletr  36154  broutsideof3  36166  opnrebl2  36361  nn0prpw  36363  fin2so  37653  poimirlem27  37693  poimirlem30  37696  poimirlem31  37697  poimir  37699  mblfinlem1  37703  mblfinlem2  37704  mblfinlem3  37705  mblfinlem4  37706  itg2addnclem  37717  ftc1cnnc  37738  ftc1anclem5  37743  sdclem1  37789  geomcau  37805  equivtotbnd  37824  bndss  37832  ismtybndlem  37852  heibor1lem  37855  rrncmslem  37878  rngo2  37953  prtlem15  38920  lsateln0  39040  lsat0cv  39078  eqlkr3  39146  lkrshp  39150  lshpset2N  39164  hlhgt2  39434  hlrelat2  39448  atle  39481  athgt  39501  2dim  39515  1cvratex  39518  ps-2  39523  dalem20  39738  lhpexle1lem  40052  lhpexle1  40053  lhpexle2lem  40054  lhpmcvr5N  40072  lhpmcvr6N  40073  cdleme25a  40398  cdleme29ex  40419  cdlemfnid  40609  cdlemg33b0  40746  cdlemg33a  40751  cdlemg35  40758  cdleml3N  41023  dihlsscpre  41279  dih1dimb2  41286  dihatexv  41383  dvh3dim2  41493  dochkr1  41523  dochkr1OLDN  41524  lcfl8  41547  lcfl8b  41549  lcfrlem5  41591  lcfrlem6  41592  mapdrvallem2  41690  mapdh9a  41834  mapdh9aOLDN  41835  hdmaprnlem3eN  41903  hdmaprnlem16N  41907  mndmolinv  42134  primrootsunit1  42136  flt4lem5elem  42690  flt4lem7  42698  nna4b4nsq  42699  fphpdo  42856  rencldnfilem  42859  irrapxlem2  42862  oasubex  43325  tfsconcatlem  43375  tfsconcatrev  43387  cvgdvgrat  44352  expgrowth  44374  projf1o  45240  ssfiunibd  45356  supxrgere  45378  supxrgelem  45382  suplesup  45384  infrpge  45396  infleinf  45416  supxrunb3  45443  unb2ltle  45459  uzub  45475  cvgcaule  45535  qinioo  45581  qelioo  45592  climinf  45652  mullimc  45662  islptre  45665  limccog  45666  mullimcf  45669  limcrecl  45675  sumnnodd  45676  neglimc  45691  0ellimcdiv  45693  limclner  45695  allbutfifvre  45719  climleltrp  45720  fnlimabslt  45723  climinf2lem  45750  limsuppnflem  45754  limsupvaluz2  45782  supcnvlimsup  45784  limsupgtlem  45821  liminflelimsupuz  45829  liminflimsupclim  45851  limsupub2  45856  xlimpnfxnegmnf  45858  cncfioobd  45941  stoweidlem7  46051  stoweidlem27  46071  stoweidlem39  46083  stoweidlem48  46092  stoweidlem49  46093  stoweidlem60  46104  stoweidlem61  46105  stoweid  46107  dirkercncflem2  46148  fourierdlem20  46171  fourierdlem39  46190  fourierdlem41  46192  fourierdlem48  46198  fourierdlem49  46199  fourierdlem50  46200  fourierdlem64  46214  fourierdlem73  46223  fourierdlem74  46224  fourierdlem75  46225  fourierdlem87  46237  fourierdlem103  46253  fourierdlem104  46254  qndenserrnopnlem  46341  sge0ltfirp  46444  sge0gerpmpt  46446  sge0ltfirpmpt2  46470  sge0isum  46471  sge0pnffigtmpt  46484  sge0pnffsumgt  46486  sge0gtfsumgt  46487  sge0uzfsumgt  46488  nnfoctbdjlem  46499  meaiuninclem  46524  meaiuninc3v  46528  omeiunltfirp  46563  carageniuncllem2  46566  hoicvr  46592  volicorescl  46597  hoidmv1le  46638  hoidmvlelem3  46641  hoiqssbllem3  46668  hspmbllem2  46671  iunhoiioolem  46719  vonioo  46726  vonicc  46729  smfaddlem1  46807  smflimlem2  46816  smflimlem3  46817  smfmullem4  46838  fsetsnfo  47090  2reu8i  47150  imasetpreimafvbijlemfo  47442  2pwp1prmfmtno  47627  proththd  47651  sbgoldbwt  47814  sbgoldbst  47815  sbgoldbalt  47818  bgoldbtbndlem4  47845  bgoldbtbnd  47846  grtriprop  47978  ply1mulgsumlem3  48426  ply1mulgsumlem4  48427  islindeps2  48521  isldepslvec2  48523