MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximdva Structured version   Visualization version   GIF version

Theorem reximdva 3272
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
StepHypRef Expression
1 reximdva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 415 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 3270 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2108  wrex 3137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-ral 3141  df-rex 3142
This theorem is referenced by:  reximddv  3273  reximdvva  3275  reximddv2  3276  wereu2  5545  dffo4  6862  nnaordex  8256  frfi  8755  fisupg  8758  marypha1  8890  fiinfg  8955  wemapsolem  9006  unwdomg  9040  rankr1ai  9219  cofsmo  9683  cfcoflem  9686  inar1  10189  nqerf  10344  prlem936  10461  fimaxre  11576  fimaxreOLD  11577  fiminre  11580  arch  11886  bndndx  11888  suprfinzcl  12089  zmin  12336  elpq  12366  qbtwnxr  12585  qsqueeze  12586  qextltlem  12587  xrsupsslem  12692  xrinfmsslem  12693  xrub  12697  supxrunb1  12704  ssnn0fi  13345  fsuppmapnn0fiub0  13353  fsuppmapnn0fz  13356  expnlbnd2  13587  r19.29uz  14702  cau3lem  14706  rlim2lt  14846  rlimclim  14895  2clim  14921  o1co  14935  climcn1  14940  climcn2  14941  rlimo1  14965  climsqz  14989  climsqz2  14990  rlimsqzlem  14997  lo1le  15000  climsup  15018  climcau  15019  caucvgrlem2  15023  iseralt  15033  cvgcmp  15163  cvgcmpce  15165  supcvg  15203  rpnnen2lem12  15570  bezoutlem1  15879  divgcdcoprmex  16002  exprmfct  16040  prmdvdsfz  16041  pclem  16167  pc2dvds  16207  pcprmpw  16211  dvdsprmpweqle  16214  unbenlem  16236  infpnlem2  16239  infpn2  16241  prmunb  16242  vdwlem2  16310  ramub1lem2  16355  prmdvdsprmop  16371  prmgaplem7  16385  ipodrsima  17767  smndex1mgm  18064  grpinveu  18130  dfgrp3lem  18189  psgneu  18626  odbezout  18677  sylow2blem3  18739  nn0gsumfz  19096  ringadd2  19317  irredrmul  19449  lbsextlem2  19923  mptcoe1fsupp  20375  znunit  20702  scmate  21111  scmatscm  21114  scmatfo  21131  mat1scmat  21140  pmatcoe1fsupp  21301  pmatcollpwfi  21382  pmatcollpw3fi  21385  mptcoe1matfsupp  21402  pm2mp  21425  chmaidscmat  21448  cpmadumatpoly  21483  chcoeffeq  21486  cayhamlem3  21487  cayhamlem4  21488  neiptopnei  21732  neitr  21780  cnpnei  21864  haust1  21952  isnrm3  21959  isreg2  21977  tgcmp  22001  hauscmplem  22006  hauscmp  22007  bwth  22010  1stcfb  22045  1stcelcls  22061  lly1stc  22096  txcmplem1  22241  txlm  22248  xkococnlem  22259  filuni  22485  filufint  22520  ufilen  22530  fclscf  22625  cnextcn  22667  ustex2sym  22817  ustex3sym  22818  utopreg  22853  isucn2  22880  ucnima  22882  ucncn  22886  neipcfilu  22897  metequiv2  23112  metrest  23126  xrsmopn  23412  mulc1cncf  23505  cncfco  23507  bndth  23554  lmmcvg  23856  cfil3i  23864  iscau4  23874  cmetcaulem  23883  iscmet3lem1  23886  caussi  23892  equivcfil  23894  equivcau  23895  caubl  23903  minveclem3b  24023  ovolgelb  24073  ovollb2lem  24081  ovolctb  24083  ovolicc2lem4  24113  ioombl1lem4  24154  dyadmax  24191  volsup2  24198  itg2monolem1  24343  c1liplem1  24585  c1lip1  24586  dvivthlem1  24597  lhop1  24603  ftc1a  24626  ftc1lem6  24630  ply1divex  24722  elply2  24778  dgrlem  24811  aacjcl  24908  aalioulem2  24914  aalioulem3  24915  aalioulem4  24916  ulmcaulem  24974  ulmcau  24975  ulmss  24977  mtest  24984  itgulm  24988  reeff1o  25027  efif1olem4  25121  rlimcnp  25535  xrlimcnp  25538  lgamucov  25607  ftalem3  25644  fta  25649  muval1  25702  dvdssqf  25707  mumullem1  25748  lgsqrmod  25920  lgsqrmodndvds  25921  pntlem3  26177  ostth  26207  tgtrisegint  26277  tgbtwndiff  26284  tgcgrxfr  26296  lnext  26345  legov2  26364  legtrd  26367  hlcgrex  26394  colperpexlem3  26510  colperpex  26511  hlpasch  26534  hpgerlem  26543  hpgtr  26546  dfcgra2  26608  acopy  26611  inagswap  26619  inaghl  26623  cgrg3col4  26631  axpasch  26719  wwlksnredwwlkn0  27666  midwwlks2s3  27723  clwwlkn1loopb  27813  2pthfrgrrn2  28054  frgrwopreg1  28089  frgrwopreg2  28090  grpoidinvlem3  28275  grpoideu  28278  grpoinveu  28288  ubthlem1  28639  minvecolem5  28650  htthlem  28686  chscllem2  29407  nmopun  29783  lnconi  29802  rnbra  29876  sumdmdii  30184  cdj3lem2b  30206  foresf1o  30257  acunirnmpt  30396  xrofsup  30484  fprodex01  30534  isarchi3  30809  isarchiofld  30883  lmxrge0  31188  lmdvg  31189  esumlub  31312  esumfsup  31322  esumcvg  31338  ftc2re  31862  cusgr3cyclex  32376  cvmliftmolem2  32522  cvmlift2lem12  32554  satfv1  32603  satffunlem1lem2  32643  satffunlem2lem2  32646  satfv0fvfmla0  32653  frpomin  33071  frmin  33077  wzel  33104  wsuclem  33105  nosupno  33196  nosupbnd1lem4  33204  conway  33257  btwndiff  33481  trisegint  33482  cgrxfr  33509  lineext  33530  segcon2  33559  brsegle2  33563  seglecgr12im  33564  segletr  33568  broutsideof3  33580  opnrebl2  33662  nn0prpw  33664  fin2so  34871  poimirlem27  34911  poimirlem30  34914  poimirlem31  34915  poimir  34917  mblfinlem1  34921  mblfinlem2  34922  mblfinlem3  34923  mblfinlem4  34924  itg2addnclem  34935  ftc1cnnc  34958  ftc1anclem5  34963  sdclem1  35010  geomcau  35026  equivtotbnd  35048  bndss  35056  ismtybndlem  35076  heibor1lem  35079  rrncmslem  35102  rngo2  35177  prtlem15  36003  lsateln0  36123  lsat0cv  36161  eqlkr3  36229  lkrshp  36233  lshpset2N  36247  hlhgt2  36517  hlrelat2  36531  atle  36564  athgt  36584  2dim  36598  1cvratex  36601  ps-2  36606  dalem20  36821  lhpexle1lem  37135  lhpexle1  37136  lhpexle2lem  37137  lhpmcvr5N  37155  lhpmcvr6N  37156  cdleme25a  37481  cdleme29ex  37502  cdlemfnid  37692  cdlemg33b0  37829  cdlemg33a  37834  cdlemg35  37841  cdleml3N  38106  dihlsscpre  38362  dih1dimb2  38369  dihatexv  38466  dvh3dim2  38576  dochkr1  38606  dochkr1OLDN  38607  lcfl8  38630  lcfl8b  38632  lcfrlem5  38674  lcfrlem6  38675  mapdrvallem2  38773  mapdh9a  38917  mapdh9aOLDN  38918  hdmaprnlem3eN  38986  hdmaprnlem16N  38990  fphpdo  39404  rencldnfilem  39407  irrapxlem2  39410  cvgdvgrat  40635  expgrowth  40657  projf1o  41448  ssfiunibd  41565  supxrgere  41590  supxrgelem  41594  suplesup  41596  infrpge  41608  infleinf  41629  supxrunb3  41661  unb2ltle  41678  uzub  41694  qinioo  41800  qelioo  41811  climinf  41876  mullimc  41886  islptre  41889  limccog  41890  mullimcf  41893  limcrecl  41899  sumnnodd  41900  neglimc  41917  0ellimcdiv  41919  limclner  41921  allbutfifvre  41945  climleltrp  41946  fnlimabslt  41949  climinf2lem  41976  limsuppnflem  41980  limsupvaluz2  42008  supcnvlimsup  42010  limsupgtlem  42047  liminflelimsupuz  42055  liminflimsupclim  42077  limsupub2  42082  xlimpnfxnegmnf  42084  cncfioobd  42169  stoweidlem7  42282  stoweidlem27  42302  stoweidlem39  42314  stoweidlem48  42323  stoweidlem49  42324  stoweidlem60  42335  stoweidlem61  42336  stoweid  42338  dirkercncflem2  42379  fourierdlem20  42402  fourierdlem39  42421  fourierdlem41  42423  fourierdlem48  42429  fourierdlem49  42430  fourierdlem50  42431  fourierdlem64  42445  fourierdlem73  42454  fourierdlem74  42455  fourierdlem75  42456  fourierdlem87  42468  fourierdlem103  42484  fourierdlem104  42485  qndenserrnopnlem  42572  sge0ltfirp  42672  sge0gerpmpt  42674  sge0ltfirpmpt2  42698  sge0isum  42699  sge0pnffigtmpt  42712  sge0pnffsumgt  42714  sge0gtfsumgt  42715  sge0uzfsumgt  42716  nnfoctbdjlem  42727  meaiuninclem  42752  meaiuninc3v  42756  omeiunltfirp  42791  carageniuncllem2  42794  hoicvr  42820  volicorescl  42825  hoidmv1le  42866  hoidmvlelem3  42869  hoiqssbllem3  42896  hspmbllem2  42899  iunhoiioolem  42947  vonioo  42954  vonicc  42957  smfaddlem1  43029  smflimlem2  43038  smflimlem3  43039  smfmullem4  43059  2reu8i  43302  imasetpreimafvbijlemfo  43555  2pwp1prmfmtno  43742  proththd  43769  sbgoldbwt  43932  sbgoldbst  43933  sbgoldbalt  43936  bgoldbtbndlem4  43963  bgoldbtbnd  43964  zrninitoringc  44332  ply1mulgsumlem3  44432  ply1mulgsumlem4  44433  islindeps2  44528  isldepslvec2  44530
  Copyright terms: Public domain W3C validator