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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  reximddv  3156  reximdvva  3188  reximddv2  3199  wereu2  5622  frpomin  6298  dffo4  7051  nnaordex  8571  frfi  9192  fisupg  9195  marypha1  9344  fiinfg  9411  wemapsolem  9462  unwdomg  9496  rankr1ai  9720  cofsmo  10189  cfcoflem  10192  inar1  10696  nqerf  10851  prlem936  10968  fimaxre  12098  fiminre  12101  arch  12432  bndndx  12434  suprfinzcl  12641  zmin  12892  elpq  12923  qbtwnxr  13150  qsqueeze  13151  qextltlem  13152  xrsupsslem  13257  xrinfmsslem  13258  xrub  13262  supxrunb1  13269  ssnn0fi  13945  fsuppmapnn0fiub0  13953  fsuppmapnn0fz  13956  expnlbnd2  14194  r19.29uz  15311  cau3lem  15315  rlim2lt  15457  rlimclim  15506  2clim  15532  o1co  15546  climcn1  15552  climcn2  15553  rlimo1  15577  climsqz  15601  climsqz2  15602  rlimsqzlem  15609  lo1le  15612  climsup  15630  climcau  15631  caucvgrlem2  15635  iseralt  15645  cvgcmp  15777  cvgcmpce  15779  supcvg  15819  rpnnen2lem12  16190  bezoutlem1  16506  divgcdcoprmex  16633  exprmfct  16672  prmdvdsfz  16673  prmdvdsncoprmbd  16695  pclem  16807  pc2dvds  16848  pcprmpw  16852  dvdsprmpweqle  16855  unbenlem  16877  infpnlem2  16880  infpn2  16882  prmunb  16883  vdwlem2  16951  ramub1lem2  16996  prmdvdsprmop  17012  prmgaplem7  17026  ipodrsima  18505  smndex1mgm  18876  grpinveu  18948  dfgrp3lem  19012  psgneu  19479  odbezout  19531  sylow2blem3  19595  nn0gsumfz  19957  irredrmul  20405  zrninitoringc  20655  lbsextlem2  21159  znunit  21545  mptcoe1fsupp  22207  evls1fpws  22362  scmate  22500  scmatscm  22503  scmatfo  22520  mat1scmat  22529  pmatcoe1fsupp  22691  pmatcollpwfi  22772  pmatcollpw3fi  22775  mptcoe1matfsupp  22792  pm2mp  22815  chmaidscmat  22838  cpmadumatpoly  22873  chcoeffeq  22876  cayhamlem3  22877  cayhamlem4  22878  neiptopnei  23122  neitr  23170  cnpnei  23254  haust1  23342  isnrm3  23349  isreg2  23367  tgcmp  23391  hauscmplem  23396  hauscmp  23397  bwth  23400  1stcfb  23435  1stcelcls  23451  lly1stc  23486  txcmplem1  23631  txlm  23638  xkococnlem  23649  filuni  23875  filufint  23910  ufilen  23920  fclscf  24015  cnextcn  24057  ustex2sym  24207  ustex3sym  24208  utopreg  24242  isucn2  24268  ucnima  24270  ucncn  24274  neipcfilu  24285  metequiv2  24500  metrest  24514  xrsmopn  24803  mulc1cncf  24897  cncfco  24899  bndth  24950  lmmcvg  25253  cfil3i  25261  iscau4  25271  cmetcaulem  25280  iscmet3lem1  25283  caussi  25289  equivcfil  25291  equivcau  25292  caubl  25300  minveclem3b  25420  ovolgelb  25472  ovollb2lem  25480  ovolctb  25482  ovolicc2lem4  25512  ioombl1lem4  25553  dyadmax  25590  volsup2  25597  itg2monolem1  25742  c1liplem1  25988  c1lip1  25989  dvivthlem1  26000  lhop1  26006  ftc1a  26029  ftc1lem6  26033  ply1divex  26127  elply2  26186  dgrlem  26219  aacjcl  26318  aalioulem2  26324  aalioulem3  26325  aalioulem4  26326  ulmcaulem  26384  ulmcau  26385  ulmss  26387  mtest  26394  itgulm  26398  reeff1o  26437  efif1olem4  26534  rlimcnp  26954  xrlimcnp  26957  lgamucov  27026  ftalem3  27063  fta  27068  muval1  27121  dvdssqf  27126  mumullem1  27167  lgsqrmod  27340  lgsqrmodndvds  27341  pntlem3  27597  ostth  27627  nosupno  27692  nosupbnd1lem4  27700  noinfno  27707  noinfbnd1lem4  27715  conway  27796  etaslts  27810  znegscl  28409  tgtrisegint  28592  tgbtwndiff  28599  tgcgrxfr  28611  lnext  28660  legov2  28679  legtrd  28682  hlcgrex  28709  colperpexlem3  28825  colperpex  28826  hlpasch  28849  hpgerlem  28858  hpgtr  28861  dfcgra2  28923  acopy  28926  inagswap  28934  inaghl  28938  cgrg3col4  28946  axpasch  29035  wwlksnredwwlkn0  29989  midwwlks2s3  30045  clwwlkn1loopb  30138  2pthfrgrrn2  30378  frgrwopreg1  30413  frgrwopreg2  30414  grpoidinvlem3  30602  grpoideu  30605  grpoinveu  30615  ubthlem1  30966  minvecolem5  30977  htthlem  31013  chscllem2  31734  nmopun  32110  lnconi  32129  rnbra  32203  sumdmdii  32511  cdj3lem2b  32533  foresf1o  32599  acunirnmpt  32758  xrofsup  32866  fprodex01  32924  mndlactfo  33113  mndractfo  33115  isarchi3  33275  isarchiofld  33287  erler  33353  dfufd2lem  33639  constrconj  33936  constrextdg2lem  33939  constrcjcl  33959  lmxrge0  34143  lmdvg  34144  esumlub  34251  esumfsup  34261  esumcvg  34277  ftc2re  34789  cusgr3cyclex  35371  cvmliftmolem2  35517  cvmlift2lem12  35549  satfv1  35598  satffunlem1lem2  35638  satffunlem2lem2  35641  satfv0fvfmla0  35648  ellcsrspsn  35876  r1peuqusdeg1  35878  wzel  36057  wsuclem  36058  btwndiff  36262  trisegint  36263  cgrxfr  36290  lineext  36311  segcon2  36340  brsegle2  36344  seglecgr12im  36345  segletr  36349  broutsideof3  36361  opnrebl2  36556  nn0prpw  36558  fin2so  37981  poimirlem27  38021  poimirlem30  38024  poimirlem31  38025  poimir  38027  mblfinlem1  38031  mblfinlem2  38032  mblfinlem3  38033  mblfinlem4  38034  itg2addnclem  38045  ftc1cnnc  38066  ftc1anclem5  38071  sdclem1  38117  geomcau  38133  equivtotbnd  38152  bndss  38160  ismtybndlem  38180  heibor1lem  38183  rrncmslem  38206  rngo2  38281  prtlem15  39374  lsateln0  39494  lsat0cv  39532  eqlkr3  39600  lkrshp  39604  lshpset2N  39618  hlhgt2  39888  hlrelat2  39902  atle  39935  athgt  39955  2dim  39969  1cvratex  39972  ps-2  39977  dalem20  40192  lhpexle1lem  40506  lhpexle1  40507  lhpexle2lem  40508  lhpmcvr5N  40526  lhpmcvr6N  40527  cdleme25a  40852  cdleme29ex  40873  cdlemfnid  41063  cdlemg33b0  41200  cdlemg33a  41205  cdlemg35  41212  cdleml3N  41477  dihlsscpre  41733  dih1dimb2  41740  dihatexv  41837  dvh3dim2  41947  dochkr1  41977  dochkr1OLDN  41978  lcfl8  42001  lcfl8b  42003  lcfrlem5  42045  lcfrlem6  42046  mapdrvallem2  42144  mapdh9a  42288  mapdh9aOLDN  42289  hdmaprnlem3eN  42357  hdmaprnlem16N  42361  mndmolinv  42587  primrootsunit1  42589  flt4lem5elem  43108  flt4lem7  43116  nna4b4nsq  43117  fphpdo  43269  rencldnfilem  43272  irrapxlem2  43275  oasubex  43738  tfsconcatlem  43788  tfsconcatrev  43800  cvgdvgrat  44764  expgrowth  44786  projf1o  45650  ssfiunibd  45764  supxrgere  45785  supxrgelem  45789  suplesup  45791  infrpge  45803  infleinf  45823  supxrunb3  45850  unb2ltle  45865  uzub  45881  cvgcaule  45941  qinioo  45987  qelioo  45998  climinf  46058  mullimc  46068  islptre  46071  limccog  46072  mullimcf  46075  limcrecl  46081  sumnnodd  46082  neglimc  46097  0ellimcdiv  46099  limclner  46101  allbutfifvre  46125  climleltrp  46126  fnlimabslt  46129  climinf2lem  46156  limsuppnflem  46160  limsupvaluz2  46188  supcnvlimsup  46190  limsupgtlem  46227  liminflelimsupuz  46235  liminflimsupclim  46257  limsupub2  46262  xlimpnfxnegmnf  46264  cncfioobd  46347  stoweidlem7  46457  stoweidlem27  46477  stoweidlem39  46489  stoweidlem48  46498  stoweidlem49  46499  stoweidlem60  46510  stoweidlem61  46511  stoweid  46513  dirkercncflem2  46554  fourierdlem20  46577  fourierdlem39  46596  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem64  46620  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem87  46643  fourierdlem103  46659  fourierdlem104  46660  qndenserrnopnlem  46747  sge0ltfirp  46850  sge0gerpmpt  46852  sge0ltfirpmpt2  46876  sge0isum  46877  sge0pnffigtmpt  46890  sge0pnffsumgt  46892  sge0gtfsumgt  46893  sge0uzfsumgt  46894  nnfoctbdjlem  46905  meaiuninclem  46930  meaiuninc3v  46934  omeiunltfirp  46969  carageniuncllem2  46972  volicorescl  47003  hoidmv1le  47044  hoidmvlelem3  47047  hoiqssbllem3  47074  hspmbllem2  47077  iunhoiioolem  47125  vonioo  47132  vonicc  47135  smfaddlem1  47213  smflimlem2  47222  smflimlem3  47223  smfmullem4  47244  fsetsnfo  47523  2reu8i  47583  imasetpreimafvbijlemfo  47887  2pwp1prmfmtno  48075  proththd  48099  sbgoldbwt  48275  sbgoldbst  48276  sbgoldbalt  48279  bgoldbtbndlem4  48306  bgoldbtbnd  48307  grtriprop  48439  ply1mulgsumlem3  48886  ply1mulgsumlem4  48887  islindeps2  48981  isldepslvec2  48983