Theorem reximdva 3276

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
reximdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
reximdva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		reximdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 415	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3274	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3141

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 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  reximddv  3277  reximdvva  3279  reximddv2  3280  wereu2  5554  dffo4  6871  nnaordex  8266  frfi  8765  fisupg  8768  marypha1  8900  fiinfg  8965  wemapsolem  9016  unwdomg  9050  rankr1ai  9229  cofsmo  9693  cfcoflem  9696  inar1  10199  nqerf  10354  prlem936  10471  fimaxre  11586  fimaxreOLD  11587  fiminre  11590  arch  11897  bndndx  11899  suprfinzcl  12100  zmin  12347  elpq  12377  qbtwnxr  12596  qsqueeze  12597  qextltlem  12598  xrsupsslem  12703  xrinfmsslem  12704  xrub  12708  supxrunb1  12715  ssnn0fi  13356  fsuppmapnn0fiub0  13364  fsuppmapnn0fz  13367  expnlbnd2  13598  r19.29uz  14712  cau3lem  14716  rlim2lt  14856  rlimclim  14905  2clim  14931  o1co  14945  climcn1  14950  climcn2  14951  rlimo1  14975  climsqz  14999  climsqz2  15000  rlimsqzlem  15007  lo1le  15010  climsup  15028  climcau  15029  caucvgrlem2  15033  iseralt  15043  cvgcmp  15173  cvgcmpce  15175  supcvg  15213  rpnnen2lem12  15580  bezoutlem1  15889  divgcdcoprmex  16012  exprmfct  16050  prmdvdsfz  16051  pclem  16177  pc2dvds  16217  pcprmpw  16221  dvdsprmpweqle  16224  unbenlem  16246  infpnlem2  16249  infpn2  16251  prmunb  16252  vdwlem2  16320  ramub1lem2  16365  prmdvdsprmop  16381  prmgaplem7  16395  ipodrsima  17777  smndex1mgm  18074  grpinveu  18140  dfgrp3lem  18199  psgneu  18636  odbezout  18687  sylow2blem3  18749  nn0gsumfz  19106  ringadd2  19327  irredrmul  19459  lbsextlem2  19933  mptcoe1fsupp  20385  znunit  20712  scmate  21121  scmatscm  21124  scmatfo  21141  mat1scmat  21150  pmatcoe1fsupp  21311  pmatcollpwfi  21392  pmatcollpw3fi  21395  mptcoe1matfsupp  21412  pm2mp  21435  chmaidscmat  21458  cpmadumatpoly  21493  chcoeffeq  21496  cayhamlem3  21497  cayhamlem4  21498  neiptopnei  21742  neitr  21790  cnpnei  21874  haust1  21962  isnrm3  21969  isreg2  21987  tgcmp  22011  hauscmplem  22016  hauscmp  22017  bwth  22020  1stcfb  22055  1stcelcls  22071  lly1stc  22106  txcmplem1  22251  txlm  22258  xkococnlem  22269  filuni  22495  filufint  22530  ufilen  22540  fclscf  22635  cnextcn  22677  ustex2sym  22827  ustex3sym  22828  utopreg  22863  isucn2  22890  ucnima  22892  ucncn  22896  neipcfilu  22907  metequiv2  23122  metrest  23136  xrsmopn  23422  mulc1cncf  23515  cncfco  23517  bndth  23564  lmmcvg  23866  cfil3i  23874  iscau4  23884  cmetcaulem  23893  iscmet3lem1  23896  caussi  23902  equivcfil  23904  equivcau  23905  caubl  23913  minveclem3b  24033  ovolgelb  24083  ovollb2lem  24091  ovolctb  24093  ovolicc2lem4  24123  ioombl1lem4  24164  dyadmax  24201  volsup2  24208  itg2monolem1  24353  c1liplem1  24595  c1lip1  24596  dvivthlem1  24607  lhop1  24613  ftc1a  24636  ftc1lem6  24640  ply1divex  24732  elply2  24788  dgrlem  24821  aacjcl  24918  aalioulem2  24924  aalioulem3  24925  aalioulem4  24926  ulmcaulem  24984  ulmcau  24985  ulmss  24987  mtest  24994  itgulm  24998  reeff1o  25037  efif1olem4  25131  rlimcnp  25545  xrlimcnp  25548  lgamucov  25617  ftalem3  25654  fta  25659  muval1  25712  dvdssqf  25717  mumullem1  25758  lgsqrmod  25930  lgsqrmodndvds  25931  pntlem3  26187  ostth  26217  tgtrisegint  26287  tgbtwndiff  26294  tgcgrxfr  26306  lnext  26355  legov2  26374  legtrd  26377  hlcgrex  26404  colperpexlem3  26520  colperpex  26521  hlpasch  26544  hpgerlem  26553  hpgtr  26556  dfcgra2  26618  acopy  26621  inagswap  26629  inaghl  26633  cgrg3col4  26641  axpasch  26729  wwlksnredwwlkn0  27676  midwwlks2s3  27733  clwwlkn1loopb  27823  2pthfrgrrn2  28064  frgrwopreg1  28099  frgrwopreg2  28100  grpoidinvlem3  28285  grpoideu  28288  grpoinveu  28298  ubthlem1  28649  minvecolem5  28660  htthlem  28696  chscllem2  29417  nmopun  29793  lnconi  29812  rnbra  29886  sumdmdii  30194  cdj3lem2b  30216  foresf1o  30267  acunirnmpt  30406  xrofsup  30494  fprodex01  30543  isarchi3  30818  isarchiofld  30892  lmxrge0  31197  lmdvg  31198  esumlub  31321  esumfsup  31331  esumcvg  31347  ftc2re  31871  cusgr3cyclex  32385  cvmliftmolem2  32531  cvmlift2lem12  32563  satfv1  32612  satffunlem1lem2  32652  satffunlem2lem2  32655  satfv0fvfmla0  32662  frpomin  33080  frmin  33086  wzel  33113  wsuclem  33114  nosupno  33205  nosupbnd1lem4  33213  conway  33266  btwndiff  33490  trisegint  33491  cgrxfr  33518  lineext  33539  segcon2  33568  brsegle2  33572  seglecgr12im  33573  segletr  33577  broutsideof3  33589  opnrebl2  33671  nn0prpw  33673  fin2so  34881  poimirlem27  34921  poimirlem30  34924  poimirlem31  34925  poimir  34927  mblfinlem1  34931  mblfinlem2  34932  mblfinlem3  34933  mblfinlem4  34934  itg2addnclem  34945  ftc1cnnc  34968  ftc1anclem5  34973  sdclem1  35020  geomcau  35036  equivtotbnd  35058  bndss  35066  ismtybndlem  35086  heibor1lem  35089  rrncmslem  35112  rngo2  35187  prtlem15  36013  lsateln0  36133  lsat0cv  36171  eqlkr3  36239  lkrshp  36243  lshpset2N  36257  hlhgt2  36527  hlrelat2  36541  atle  36574  athgt  36594  2dim  36608  1cvratex  36611  ps-2  36616  dalem20  36831  lhpexle1lem  37145  lhpexle1  37146  lhpexle2lem  37147  lhpmcvr5N  37165  lhpmcvr6N  37166  cdleme25a  37491  cdleme29ex  37512  cdlemfnid  37702  cdlemg33b0  37839  cdlemg33a  37844  cdlemg35  37851  cdleml3N  38116  dihlsscpre  38372  dih1dimb2  38379  dihatexv  38476  dvh3dim2  38586  dochkr1  38616  dochkr1OLDN  38617  lcfl8  38640  lcfl8b  38642  lcfrlem5  38684  lcfrlem6  38685  mapdrvallem2  38783  mapdh9a  38927  mapdh9aOLDN  38928  hdmaprnlem3eN  38996  hdmaprnlem16N  39000  fphpdo  39421  rencldnfilem  39424  irrapxlem2  39427  cvgdvgrat  40652  expgrowth  40674  projf1o  41466  ssfiunibd  41583  supxrgere  41608  supxrgelem  41612  suplesup  41614  infrpge  41626  infleinf  41647  supxrunb3  41679  unb2ltle  41696  uzub  41712  qinioo  41818  qelioo  41829  climinf  41894  mullimc  41904  islptre  41907  limccog  41908  mullimcf  41911  limcrecl  41917  sumnnodd  41918  neglimc  41935  0ellimcdiv  41937  limclner  41939  allbutfifvre  41963  climleltrp  41964  fnlimabslt  41967  climinf2lem  41994  limsuppnflem  41998  limsupvaluz2  42026  supcnvlimsup  42028  limsupgtlem  42065  liminflelimsupuz  42073  liminflimsupclim  42095  limsupub2  42100  xlimpnfxnegmnf  42102  cncfioobd  42187  stoweidlem7  42299  stoweidlem27  42319  stoweidlem39  42331  stoweidlem48  42340  stoweidlem49  42341  stoweidlem60  42352  stoweidlem61  42353  stoweid  42355  dirkercncflem2  42396  fourierdlem20  42419  fourierdlem39  42438  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem50  42448  fourierdlem64  42462  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem87  42485  fourierdlem103  42501  fourierdlem104  42502  qndenserrnopnlem  42589  sge0ltfirp  42689  sge0gerpmpt  42691  sge0ltfirpmpt2  42715  sge0isum  42716  sge0pnffigtmpt  42729  sge0pnffsumgt  42731  sge0gtfsumgt  42732  sge0uzfsumgt  42733  nnfoctbdjlem  42744  meaiuninclem  42769  meaiuninc3v  42773  omeiunltfirp  42808  carageniuncllem2  42811  hoicvr  42837  volicorescl  42842  hoidmv1le  42883  hoidmvlelem3  42886  hoiqssbllem3  42913  hspmbllem2  42916  iunhoiioolem  42964  vonioo  42971  vonicc  42974  smfaddlem1  43046  smflimlem2  43055  smflimlem3  43056  smfmullem4  43076  2reu8i  43319  imasetpreimafvbijlemfo  43572  2pwp1prmfmtno  43759  proththd  43786  sbgoldbwt  43949  sbgoldbst  43950  sbgoldbalt  43953  bgoldbtbndlem4  43980  bgoldbtbnd  43981  zrninitoringc  44349  ply1mulgsumlem3  44449  ply1mulgsumlem4  44450  islindeps2  44545  isldepslvec2  44547