Theorem reximdva 3167

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

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

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 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  reximddv  3170  reximdvva  3204  reximddv2  3211  wereu2  5673  frpomin  6341  dffo4  7104  nnaordex  8644  frfi  9294  fisupg  9297  marypha1  9435  fiinfg  9500  wemapsolem  9551  unwdomg  9585  rankr1ai  9799  cofsmo  10270  cfcoflem  10273  inar1  10776  nqerf  10931  prlem936  11048  fimaxre  12165  fiminre  12168  arch  12476  bndndx  12478  suprfinzcl  12683  zmin  12935  elpq  12966  qbtwnxr  13186  qsqueeze  13187  qextltlem  13188  xrsupsslem  13293  xrinfmsslem  13294  xrub  13298  supxrunb1  13305  ssnn0fi  13957  fsuppmapnn0fiub0  13965  fsuppmapnn0fz  13968  expnlbnd2  14204  r19.29uz  15304  cau3lem  15308  rlim2lt  15448  rlimclim  15497  2clim  15523  o1co  15537  climcn1  15543  climcn2  15544  rlimo1  15568  climsqz  15592  climsqz2  15593  rlimsqzlem  15602  lo1le  15605  climsup  15623  climcau  15624  caucvgrlem2  15628  iseralt  15638  cvgcmp  15769  cvgcmpce  15771  supcvg  15809  rpnnen2lem12  16175  bezoutlem1  16488  divgcdcoprmex  16610  exprmfct  16648  prmdvdsfz  16649  prmdvdsncoprmbd  16670  pclem  16778  pc2dvds  16819  pcprmpw  16823  dvdsprmpweqle  16826  unbenlem  16848  infpnlem2  16851  infpn2  16853  prmunb  16854  vdwlem2  16922  ramub1lem2  16967  prmdvdsprmop  16983  prmgaplem7  16997  ipodrsima  18504  smndex1mgm  18830  grpinveu  18902  dfgrp3lem  18964  psgneu  19422  odbezout  19474  sylow2blem3  19538  nn0gsumfz  19900  irredrmul  20325  zrninitoringc  20568  lbsextlem2  21006  znunit  21430  mptcoe1fsupp  22059  scmate  22333  scmatscm  22336  scmatfo  22353  mat1scmat  22362  pmatcoe1fsupp  22524  pmatcollpwfi  22605  pmatcollpw3fi  22608  mptcoe1matfsupp  22625  pm2mp  22648  chmaidscmat  22671  cpmadumatpoly  22706  chcoeffeq  22709  cayhamlem3  22710  cayhamlem4  22711  neiptopnei  22957  neitr  23005  cnpnei  23089  haust1  23177  isnrm3  23184  isreg2  23202  tgcmp  23226  hauscmplem  23231  hauscmp  23232  bwth  23235  1stcfb  23270  1stcelcls  23286  lly1stc  23321  txcmplem1  23466  txlm  23473  xkococnlem  23484  filuni  23710  filufint  23745  ufilen  23755  fclscf  23850  cnextcn  23892  ustex2sym  24042  ustex3sym  24043  utopreg  24078  isucn2  24105  ucnima  24107  ucncn  24111  neipcfilu  24122  metequiv2  24340  metrest  24354  xrsmopn  24649  mulc1cncf  24746  cncfco  24748  bndth  24805  lmmcvg  25110  cfil3i  25118  iscau4  25128  cmetcaulem  25137  iscmet3lem1  25140  caussi  25146  equivcfil  25148  equivcau  25149  caubl  25157  minveclem3b  25277  ovolgelb  25330  ovollb2lem  25338  ovolctb  25340  ovolicc2lem4  25370  ioombl1lem4  25411  dyadmax  25448  volsup2  25455  itg2monolem1  25601  c1liplem1  25850  c1lip1  25851  dvivthlem1  25862  lhop1  25868  ftc1a  25893  ftc1lem6  25897  ply1divex  25993  elply2  26049  dgrlem  26082  aacjcl  26180  aalioulem2  26186  aalioulem3  26187  aalioulem4  26188  ulmcaulem  26246  ulmcau  26247  ulmss  26249  mtest  26256  itgulm  26260  reeff1o  26300  efif1olem4  26395  rlimcnp  26812  xrlimcnp  26815  lgamucov  26885  ftalem3  26922  fta  26927  muval1  26980  dvdssqf  26985  mumullem1  27026  lgsqrmod  27200  lgsqrmodndvds  27201  pntlem3  27457  ostth  27487  nosupno  27551  nosupbnd1lem4  27559  noinfno  27566  noinfbnd1lem4  27574  conway  27647  etasslt  27661  tgtrisegint  28185  tgbtwndiff  28192  tgcgrxfr  28204  lnext  28253  legov2  28272  legtrd  28275  hlcgrex  28302  colperpexlem3  28418  colperpex  28419  hlpasch  28442  hpgerlem  28451  hpgtr  28454  dfcgra2  28516  acopy  28519  inagswap  28527  inaghl  28531  cgrg3col4  28539  axpasch  28634  wwlksnredwwlkn0  29585  midwwlks2s3  29641  clwwlkn1loopb  29731  2pthfrgrrn2  29971  frgrwopreg1  30006  frgrwopreg2  30007  grpoidinvlem3  30194  grpoideu  30197  grpoinveu  30207  ubthlem1  30558  minvecolem5  30569  htthlem  30605  chscllem2  31326  nmopun  31702  lnconi  31721  rnbra  31795  sumdmdii  32103  cdj3lem2b  32125  foresf1o  32177  acunirnmpt  32319  xrofsup  32415  fprodex01  32466  isarchi3  32771  isarchiofld  32873  evls1fpws  33088  lmxrge0  33398  lmdvg  33399  esumlub  33524  esumfsup  33534  esumcvg  33550  ftc2re  34076  cusgr3cyclex  34593  cvmliftmolem2  34739  cvmlift2lem12  34771  satfv1  34820  satffunlem1lem2  34860  satffunlem2lem2  34863  satfv0fvfmla0  34870  wzel  35268  wsuclem  35269  btwndiff  35471  trisegint  35472  cgrxfr  35499  lineext  35520  segcon2  35549  brsegle2  35553  seglecgr12im  35554  segletr  35558  broutsideof3  35570  opnrebl2  35673  nn0prpw  35675  fin2so  36942  poimirlem27  36982  poimirlem30  36985  poimirlem31  36986  poimir  36988  mblfinlem1  36992  mblfinlem2  36993  mblfinlem3  36994  mblfinlem4  36995  itg2addnclem  37006  ftc1cnnc  37027  ftc1anclem5  37032  sdclem1  37078  geomcau  37094  equivtotbnd  37113  bndss  37121  ismtybndlem  37141  heibor1lem  37144  rrncmslem  37167  rngo2  37242  prtlem15  38212  lsateln0  38332  lsat0cv  38370  eqlkr3  38438  lkrshp  38442  lshpset2N  38456  hlhgt2  38727  hlrelat2  38741  atle  38774  athgt  38794  2dim  38808  1cvratex  38811  ps-2  38816  dalem20  39031  lhpexle1lem  39345  lhpexle1  39346  lhpexle2lem  39347  lhpmcvr5N  39365  lhpmcvr6N  39366  cdleme25a  39691  cdleme29ex  39712  cdlemfnid  39902  cdlemg33b0  40039  cdlemg33a  40044  cdlemg35  40051  cdleml3N  40316  dihlsscpre  40572  dih1dimb2  40579  dihatexv  40676  dvh3dim2  40786  dochkr1  40816  dochkr1OLDN  40817  lcfl8  40840  lcfl8b  40842  lcfrlem5  40884  lcfrlem6  40885  mapdrvallem2  40983  mapdh9a  41127  mapdh9aOLDN  41128  hdmaprnlem3eN  41196  hdmaprnlem16N  41200  flt4lem5elem  41859  flt4lem7  41867  nna4b4nsq  41868  fphpdo  42021  rencldnfilem  42024  irrapxlem2  42027  oasubex  42502  tfsconcatlem  42552  tfsconcatrev  42564  cvgdvgrat  43538  expgrowth  43560  projf1o  44358  ssfiunibd  44481  supxrgere  44505  supxrgelem  44509  suplesup  44511  infrpge  44523  infleinf  44544  supxrunb3  44571  unb2ltle  44587  uzub  44603  cvgcaule  44664  qinioo  44710  qelioo  44721  climinf  44784  mullimc  44794  islptre  44797  limccog  44798  mullimcf  44801  limcrecl  44807  sumnnodd  44808  neglimc  44825  0ellimcdiv  44827  limclner  44829  allbutfifvre  44853  climleltrp  44854  fnlimabslt  44857  climinf2lem  44884  limsuppnflem  44888  limsupvaluz2  44916  supcnvlimsup  44918  limsupgtlem  44955  liminflelimsupuz  44963  liminflimsupclim  44985  limsupub2  44990  xlimpnfxnegmnf  44992  cncfioobd  45075  stoweidlem7  45185  stoweidlem27  45205  stoweidlem39  45217  stoweidlem48  45226  stoweidlem49  45227  stoweidlem60  45238  stoweidlem61  45239  stoweid  45241  dirkercncflem2  45282  fourierdlem20  45305  fourierdlem39  45324  fourierdlem41  45326  fourierdlem48  45332  fourierdlem49  45333  fourierdlem50  45334  fourierdlem64  45348  fourierdlem73  45357  fourierdlem74  45358  fourierdlem75  45359  fourierdlem87  45371  fourierdlem103  45387  fourierdlem104  45388  qndenserrnopnlem  45475  sge0ltfirp  45578  sge0gerpmpt  45580  sge0ltfirpmpt2  45604  sge0isum  45605  sge0pnffigtmpt  45618  sge0pnffsumgt  45620  sge0gtfsumgt  45621  sge0uzfsumgt  45622  nnfoctbdjlem  45633  meaiuninclem  45658  meaiuninc3v  45662  omeiunltfirp  45697  carageniuncllem2  45700  hoicvr  45726  volicorescl  45731  hoidmv1le  45772  hoidmvlelem3  45775  hoiqssbllem3  45802  hspmbllem2  45805  iunhoiioolem  45853  vonioo  45860  vonicc  45863  smfaddlem1  45941  smflimlem2  45950  smflimlem3  45951  smfmullem4  45972  fsetsnfo  46225  2reu8i  46283  imasetpreimafvbijlemfo  46535  2pwp1prmfmtno  46720  proththd  46744  sbgoldbwt  46907  sbgoldbst  46908  sbgoldbalt  46911  bgoldbtbndlem4  46938  bgoldbtbnd  46939  ply1mulgsumlem3  47234  ply1mulgsumlem4  47235  islindeps2  47329  isldepslvec2  47331