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

Theorem reximdva 3271
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 413 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 3269 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3140  df-rex 3141
This theorem is referenced by:  reximddv  3272  reximdvva  3274  reximddv2  3275  wereu2  5545  dffo4  6861  nnaordex  8253  frfi  8751  fisupg  8754  marypha1  8886  fiinfg  8951  wemapsolem  9002  unwdomg  9036  rankr1ai  9215  cofsmo  9679  cfcoflem  9682  inar1  10185  nqerf  10340  prlem936  10457  fimaxre  11572  fimaxreOLD  11573  fiminre  11576  arch  11882  bndndx  11884  suprfinzcl  12085  zmin  12332  elpq  12362  qbtwnxr  12581  qsqueeze  12582  qextltlem  12583  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  supxrunb1  12700  ssnn0fi  13341  fsuppmapnn0fiub0  13349  fsuppmapnn0fz  13352  expnlbnd2  13583  r19.29uz  14698  cau3lem  14702  rlim2lt  14842  rlimclim  14891  2clim  14917  o1co  14931  climcn1  14936  climcn2  14937  rlimo1  14961  climsqz  14985  climsqz2  14986  rlimsqzlem  14993  lo1le  14996  climsup  15014  climcau  15015  caucvgrlem2  15019  iseralt  15029  cvgcmp  15159  cvgcmpce  15161  supcvg  15199  rpnnen2lem12  15566  bezoutlem1  15875  divgcdcoprmex  15998  exprmfct  16036  prmdvdsfz  16037  pclem  16163  pc2dvds  16203  pcprmpw  16207  dvdsprmpweqle  16210  unbenlem  16232  infpnlem2  16235  infpn2  16237  prmunb  16238  vdwlem2  16306  ramub1lem2  16351  prmdvdsprmop  16367  prmgaplem7  16381  ipodrsima  17763  grpinveu  18076  dfgrp3lem  18135  psgneu  18563  odbezout  18614  sylow2blem3  18676  nn0gsumfz  19033  ringadd2  19254  irredrmul  19386  lbsextlem2  19860  mptcoe1fsupp  20311  znunit  20638  scmate  21047  scmatscm  21050  scmatfo  21067  mat1scmat  21076  pmatcoe1fsupp  21237  pmatcollpwfi  21318  pmatcollpw3fi  21321  mptcoe1matfsupp  21338  pm2mp  21361  chmaidscmat  21384  cpmadumatpoly  21419  chcoeffeq  21422  cayhamlem3  21423  cayhamlem4  21424  neiptopnei  21668  neitr  21716  cnpnei  21800  haust1  21888  isnrm3  21895  isreg2  21913  tgcmp  21937  hauscmplem  21942  hauscmp  21943  bwth  21946  1stcfb  21981  1stcelcls  21997  lly1stc  22032  txcmplem1  22177  txlm  22184  xkococnlem  22195  filuni  22421  filufint  22456  ufilen  22466  fclscf  22561  cnextcn  22603  ustex2sym  22752  ustex3sym  22753  utopreg  22788  isucn2  22815  ucnima  22817  ucncn  22821  neipcfilu  22832  metequiv2  23047  metrest  23061  xrsmopn  23347  mulc1cncf  23440  cncfco  23442  bndth  23489  lmmcvg  23791  cfil3i  23799  iscau4  23809  cmetcaulem  23818  iscmet3lem1  23821  caussi  23827  equivcfil  23829  equivcau  23830  caubl  23838  minveclem3b  23958  ovolgelb  24008  ovollb2lem  24016  ovolctb  24018  ovolicc2lem4  24048  ioombl1lem4  24089  dyadmax  24126  volsup2  24133  itg2monolem1  24278  c1liplem1  24520  c1lip1  24521  dvivthlem1  24532  lhop1  24538  ftc1a  24561  ftc1lem6  24565  ply1divex  24657  elply2  24713  dgrlem  24746  aacjcl  24843  aalioulem2  24849  aalioulem3  24850  aalioulem4  24851  ulmcaulem  24909  ulmcau  24910  ulmss  24912  mtest  24919  itgulm  24923  reeff1o  24962  efif1olem4  25056  rlimcnp  25470  xrlimcnp  25473  lgamucov  25542  ftalem3  25579  fta  25584  muval1  25637  dvdssqf  25642  mumullem1  25683  lgsqrmod  25855  lgsqrmodndvds  25856  pntlem3  26112  ostth  26142  tgtrisegint  26212  tgbtwndiff  26219  tgcgrxfr  26231  lnext  26280  legov2  26299  legtrd  26302  hlcgrex  26329  colperpexlem3  26445  colperpex  26446  hlpasch  26469  hpgerlem  26478  hpgtr  26481  dfcgra2  26543  acopy  26546  inagswap  26554  inaghl  26558  cgrg3col4  26566  axpasch  26654  wwlksnredwwlkn0  27601  midwwlks2s3  27658  clwwlkn1loopb  27748  2pthfrgrrn2  27989  frgrwopreg1  28024  frgrwopreg2  28025  grpoidinvlem3  28210  grpoideu  28213  grpoinveu  28223  ubthlem1  28574  minvecolem5  28585  htthlem  28621  chscllem2  29342  nmopun  29718  lnconi  29737  rnbra  29811  sumdmdii  30119  cdj3lem2b  30141  foresf1o  30192  acunirnmpt  30332  xrofsup  30418  fprodex01  30468  isarchi3  30743  isarchiofld  30817  lmxrge0  31094  lmdvg  31095  esumlub  31218  esumfsup  31228  esumcvg  31244  ftc2re  31768  cusgr3cyclex  32280  cvmliftmolem2  32426  cvmlift2lem12  32458  satfv1  32507  satffunlem1lem2  32547  satffunlem2lem2  32550  satfv0fvfmla0  32557  frpomin  32975  frmin  32981  wzel  33008  wsuclem  33009  nosupno  33100  nosupbnd1lem4  33108  conway  33161  btwndiff  33385  trisegint  33386  cgrxfr  33413  lineext  33434  segcon2  33463  brsegle2  33467  seglecgr12im  33468  segletr  33472  broutsideof3  33484  opnrebl2  33566  nn0prpw  33568  fin2so  34760  poimirlem27  34800  poimirlem30  34803  poimirlem31  34804  poimir  34806  mblfinlem1  34810  mblfinlem2  34811  mblfinlem3  34812  mblfinlem4  34813  itg2addnclem  34824  ftc1cnnc  34847  ftc1anclem5  34852  sdclem1  34899  geomcau  34915  equivtotbnd  34937  bndss  34945  ismtybndlem  34965  heibor1lem  34968  rrncmslem  34991  rngo2  35066  prtlem15  35891  lsateln0  36011  lsat0cv  36049  eqlkr3  36117  lkrshp  36121  lshpset2N  36135  hlhgt2  36405  hlrelat2  36419  atle  36452  athgt  36472  2dim  36486  1cvratex  36489  ps-2  36494  dalem20  36709  lhpexle1lem  37023  lhpexle1  37024  lhpexle2lem  37025  lhpmcvr5N  37043  lhpmcvr6N  37044  cdleme25a  37369  cdleme29ex  37390  cdlemfnid  37580  cdlemg33b0  37717  cdlemg33a  37722  cdlemg35  37729  cdleml3N  37994  dihlsscpre  38250  dih1dimb2  38257  dihatexv  38354  dvh3dim2  38464  dochkr1  38494  dochkr1OLDN  38495  lcfl8  38518  lcfl8b  38520  lcfrlem5  38562  lcfrlem6  38563  mapdrvallem2  38661  mapdh9a  38805  mapdh9aOLDN  38806  hdmaprnlem3eN  38874  hdmaprnlem16N  38878  fphpdo  39292  rencldnfilem  39295  irrapxlem2  39298  cvgdvgrat  40522  expgrowth  40544  projf1o  41335  ssfiunibd  41452  supxrgere  41477  supxrgelem  41481  suplesup  41483  infrpge  41495  infleinf  41516  supxrunb3  41548  unb2ltle  41565  uzub  41581  qinioo  41687  qelioo  41698  climinf  41763  mullimc  41773  islptre  41776  limccog  41777  mullimcf  41780  limcrecl  41786  sumnnodd  41787  neglimc  41804  0ellimcdiv  41806  limclner  41808  allbutfifvre  41832  climleltrp  41833  fnlimabslt  41836  climinf2lem  41863  limsuppnflem  41867  limsupvaluz2  41895  supcnvlimsup  41897  limsupgtlem  41934  liminflelimsupuz  41942  liminflimsupclim  41964  limsupub2  41969  xlimpnfxnegmnf  41971  cncfioobd  42056  stoweidlem7  42169  stoweidlem27  42189  stoweidlem39  42201  stoweidlem48  42210  stoweidlem49  42211  stoweidlem60  42222  stoweidlem61  42223  stoweid  42225  dirkercncflem2  42266  fourierdlem20  42289  fourierdlem39  42308  fourierdlem41  42310  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  fourierdlem64  42332  fourierdlem73  42341  fourierdlem74  42342  fourierdlem75  42343  fourierdlem87  42355  fourierdlem103  42371  fourierdlem104  42372  qndenserrnopnlem  42459  sge0ltfirp  42559  sge0gerpmpt  42561  sge0ltfirpmpt2  42585  sge0isum  42586  sge0pnffigtmpt  42599  sge0pnffsumgt  42601  sge0gtfsumgt  42602  sge0uzfsumgt  42603  nnfoctbdjlem  42614  meaiuninclem  42639  meaiuninc3v  42643  omeiunltfirp  42678  carageniuncllem2  42681  hoicvr  42707  volicorescl  42712  hoidmv1le  42753  hoidmvlelem3  42756  hoiqssbllem3  42783  hspmbllem2  42786  iunhoiioolem  42834  vonioo  42841  vonicc  42844  smfaddlem1  42916  smflimlem2  42925  smflimlem3  42926  smfmullem4  42946  2reu8i  43189  imasetpreimafvbijlemfo  43442  2pwp1prmfmtno  43629  proththd  43656  sbgoldbwt  43819  sbgoldbst  43820  sbgoldbalt  43823  bgoldbtbndlem4  43850  bgoldbtbnd  43851  smndex1mgm  44007  zrninitoringc  44270  ply1mulgsumlem3  44370  ply1mulgsumlem4  44371  islindeps2  44466  isldepslvec2  44468
  Copyright terms: Public domain W3C validator