Theorem reximdva 3165

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  reximddv  3168  reximdvva  3204  reximddv2  3212  wereu2  5685  frpomin  6362  dffo4  7122  nnaordex  8674  frfi  9318  fisupg  9321  marypha1  9471  fiinfg  9536  wemapsolem  9587  unwdomg  9621  rankr1ai  9835  cofsmo  10306  cfcoflem  10309  inar1  10812  nqerf  10967  prlem936  11084  fimaxre  12209  fiminre  12212  arch  12520  bndndx  12522  suprfinzcl  12729  zmin  12983  elpq  13014  qbtwnxr  13238  qsqueeze  13239  qextltlem  13240  xrsupsslem  13345  xrinfmsslem  13346  xrub  13350  supxrunb1  13357  ssnn0fi  14022  fsuppmapnn0fiub0  14030  fsuppmapnn0fz  14033  expnlbnd2  14269  r19.29uz  15385  cau3lem  15389  rlim2lt  15529  rlimclim  15578  2clim  15604  o1co  15618  climcn1  15624  climcn2  15625  rlimo1  15649  climsqz  15673  climsqz2  15674  rlimsqzlem  15681  lo1le  15684  climsup  15702  climcau  15703  caucvgrlem2  15707  iseralt  15717  cvgcmp  15848  cvgcmpce  15850  supcvg  15888  rpnnen2lem12  16257  bezoutlem1  16572  divgcdcoprmex  16699  exprmfct  16737  prmdvdsfz  16738  prmdvdsncoprmbd  16760  pclem  16871  pc2dvds  16912  pcprmpw  16916  dvdsprmpweqle  16919  unbenlem  16941  infpnlem2  16944  infpn2  16946  prmunb  16947  vdwlem2  17015  ramub1lem2  17060  prmdvdsprmop  17076  prmgaplem7  17090  ipodrsima  18598  smndex1mgm  18932  grpinveu  19004  dfgrp3lem  19068  psgneu  19538  odbezout  19590  sylow2blem3  19654  nn0gsumfz  20016  irredrmul  20443  zrninitoringc  20692  lbsextlem2  21178  znunit  21599  mptcoe1fsupp  22232  evls1fpws  22388  scmate  22531  scmatscm  22534  scmatfo  22551  mat1scmat  22560  pmatcoe1fsupp  22722  pmatcollpwfi  22803  pmatcollpw3fi  22806  mptcoe1matfsupp  22823  pm2mp  22846  chmaidscmat  22869  cpmadumatpoly  22904  chcoeffeq  22907  cayhamlem3  22908  cayhamlem4  22909  neiptopnei  23155  neitr  23203  cnpnei  23287  haust1  23375  isnrm3  23382  isreg2  23400  tgcmp  23424  hauscmplem  23429  hauscmp  23430  bwth  23433  1stcfb  23468  1stcelcls  23484  lly1stc  23519  txcmplem1  23664  txlm  23671  xkococnlem  23682  filuni  23908  filufint  23943  ufilen  23953  fclscf  24048  cnextcn  24090  ustex2sym  24240  ustex3sym  24241  utopreg  24276  isucn2  24303  ucnima  24305  ucncn  24309  neipcfilu  24320  metequiv2  24538  metrest  24552  xrsmopn  24847  mulc1cncf  24944  cncfco  24946  bndth  25003  lmmcvg  25308  cfil3i  25316  iscau4  25326  cmetcaulem  25335  iscmet3lem1  25338  caussi  25344  equivcfil  25346  equivcau  25347  caubl  25355  minveclem3b  25475  ovolgelb  25528  ovollb2lem  25536  ovolctb  25538  ovolicc2lem4  25568  ioombl1lem4  25609  dyadmax  25646  volsup2  25653  itg2monolem1  25799  c1liplem1  26049  c1lip1  26050  dvivthlem1  26061  lhop1  26067  ftc1a  26092  ftc1lem6  26096  ply1divex  26190  elply2  26249  dgrlem  26282  aacjcl  26383  aalioulem2  26389  aalioulem3  26390  aalioulem4  26391  ulmcaulem  26451  ulmcau  26452  ulmss  26454  mtest  26461  itgulm  26465  reeff1o  26505  efif1olem4  26601  rlimcnp  27022  xrlimcnp  27025  lgamucov  27095  ftalem3  27132  fta  27137  muval1  27190  dvdssqf  27195  mumullem1  27236  lgsqrmod  27410  lgsqrmodndvds  27411  pntlem3  27667  ostth  27697  nosupno  27762  nosupbnd1lem4  27770  noinfno  27777  noinfbnd1lem4  27785  conway  27858  etasslt  27872  znegscl  28392  tgtrisegint  28521  tgbtwndiff  28528  tgcgrxfr  28540  lnext  28589  legov2  28608  legtrd  28611  hlcgrex  28638  colperpexlem3  28754  colperpex  28755  hlpasch  28778  hpgerlem  28787  hpgtr  28790  dfcgra2  28852  acopy  28855  inagswap  28863  inaghl  28867  cgrg3col4  28875  axpasch  28970  wwlksnredwwlkn0  29925  midwwlks2s3  29981  clwwlkn1loopb  30071  2pthfrgrrn2  30311  frgrwopreg1  30346  frgrwopreg2  30347  grpoidinvlem3  30534  grpoideu  30537  grpoinveu  30547  ubthlem1  30898  minvecolem5  30909  htthlem  30945  chscllem2  31666  nmopun  32042  lnconi  32061  rnbra  32135  sumdmdii  32443  cdj3lem2b  32465  foresf1o  32531  acunirnmpt  32675  xrofsup  32777  fprodex01  32831  mndlactfo  33014  mndractfo  33016  isarchi3  33176  erler  33251  isarchiofld  33326  dfufd2lem  33556  constrconj  33749  lmxrge0  33912  lmdvg  33913  esumlub  34040  esumfsup  34050  esumcvg  34066  ftc2re  34591  cusgr3cyclex  35120  cvmliftmolem2  35266  cvmlift2lem12  35298  satfv1  35347  satffunlem1lem2  35387  satffunlem2lem2  35390  satfv0fvfmla0  35397  ellcsrspsn  35625  r1peuqusdeg1  35627  wzel  35805  wsuclem  35806  btwndiff  36008  trisegint  36009  cgrxfr  36036  lineext  36057  segcon2  36086  brsegle2  36090  seglecgr12im  36091  segletr  36095  broutsideof3  36107  opnrebl2  36303  nn0prpw  36305  fin2so  37593  poimirlem27  37633  poimirlem30  37636  poimirlem31  37637  poimir  37639  mblfinlem1  37643  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem  37657  ftc1cnnc  37678  ftc1anclem5  37683  sdclem1  37729  geomcau  37745  equivtotbnd  37764  bndss  37772  ismtybndlem  37792  heibor1lem  37795  rrncmslem  37818  rngo2  37893  prtlem15  38856  lsateln0  38976  lsat0cv  39014  eqlkr3  39082  lkrshp  39086  lshpset2N  39100  hlhgt2  39371  hlrelat2  39385  atle  39418  athgt  39438  2dim  39452  1cvratex  39455  ps-2  39460  dalem20  39675  lhpexle1lem  39989  lhpexle1  39990  lhpexle2lem  39991  lhpmcvr5N  40009  lhpmcvr6N  40010  cdleme25a  40335  cdleme29ex  40356  cdlemfnid  40546  cdlemg33b0  40683  cdlemg33a  40688  cdlemg35  40695  cdleml3N  40960  dihlsscpre  41216  dih1dimb2  41223  dihatexv  41320  dvh3dim2  41430  dochkr1  41460  dochkr1OLDN  41461  lcfl8  41484  lcfl8b  41486  lcfrlem5  41528  lcfrlem6  41529  mapdrvallem2  41627  mapdh9a  41771  mapdh9aOLDN  41772  hdmaprnlem3eN  41840  hdmaprnlem16N  41844  mndmolinv  42076  primrootsunit1  42078  flt4lem5elem  42637  flt4lem7  42645  nna4b4nsq  42646  fphpdo  42804  rencldnfilem  42807  irrapxlem2  42810  oasubex  43275  tfsconcatlem  43325  tfsconcatrev  43337  cvgdvgrat  44308  expgrowth  44330  projf1o  45139  ssfiunibd  45259  supxrgere  45282  supxrgelem  45286  suplesup  45288  infrpge  45300  infleinf  45321  supxrunb3  45348  unb2ltle  45364  uzub  45380  cvgcaule  45441  qinioo  45487  qelioo  45498  climinf  45561  mullimc  45571  islptre  45574  limccog  45575  mullimcf  45578  limcrecl  45584  sumnnodd  45585  neglimc  45602  0ellimcdiv  45604  limclner  45606  allbutfifvre  45630  climleltrp  45631  fnlimabslt  45634  climinf2lem  45661  limsuppnflem  45665  limsupvaluz2  45693  supcnvlimsup  45695  limsupgtlem  45732  liminflelimsupuz  45740  liminflimsupclim  45762  limsupub2  45767  xlimpnfxnegmnf  45769  cncfioobd  45852  stoweidlem7  45962  stoweidlem27  45982  stoweidlem39  45994  stoweidlem48  46003  stoweidlem49  46004  stoweidlem60  46015  stoweidlem61  46016  stoweid  46018  dirkercncflem2  46059  fourierdlem20  46082  fourierdlem39  46101  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem64  46125  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem87  46148  fourierdlem103  46164  fourierdlem104  46165  qndenserrnopnlem  46252  sge0ltfirp  46355  sge0gerpmpt  46357  sge0ltfirpmpt2  46381  sge0isum  46382  sge0pnffigtmpt  46395  sge0pnffsumgt  46397  sge0gtfsumgt  46398  sge0uzfsumgt  46399  nnfoctbdjlem  46410  meaiuninclem  46435  meaiuninc3v  46439  omeiunltfirp  46474  carageniuncllem2  46477  hoicvr  46503  volicorescl  46508  hoidmv1le  46549  hoidmvlelem3  46552  hoiqssbllem3  46579  hspmbllem2  46582  iunhoiioolem  46630  vonioo  46637  vonicc  46640  smfaddlem1  46718  smflimlem2  46727  smflimlem3  46728  smfmullem4  46749  fsetsnfo  47002  2reu8i  47062  imasetpreimafvbijlemfo  47329  2pwp1prmfmtno  47514  proththd  47538  sbgoldbwt  47701  sbgoldbst  47702  sbgoldbalt  47705  bgoldbtbndlem4  47732  bgoldbtbnd  47733  grtriprop  47845  ply1mulgsumlem3  48233  ply1mulgsumlem4  48234  islindeps2  48328  isldepslvec2  48330