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

Theorem reximdva 2999
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 448 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 2997 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  reximddv  3000  reximddv2  3001  wereu2  5025  dffo4  6268  nnaordex  7582  frfi  8067  fisupg  8070  marypha1  8200  fiinfg  8265  wemapsolem  8315  unwdomg  8349  rankr1ai  8521  cofsmo  8951  cfcoflem  8954  inar1  9453  nqerf  9608  prlem936  9725  fimaxre  10817  arch  11136  bndndx  11138  suprfinzcl  11324  zmin  11616  qbtwnxr  11864  qsqueeze  11865  qextltlem  11866  xrsupsslem  11965  xrinfmsslem  11966  xrub  11970  supxrunb1  11977  ssnn0fi  12601  fsuppmapnn0fiub0  12610  fsuppmapnn0fz  12613  expnlbnd2  12812  r19.29uz  13884  cau3lem  13888  rlim2lt  14022  rlimclim  14071  2clim  14097  o1co  14111  climcn1  14116  climcn2  14117  rlimo1  14141  climsqz  14165  climsqz2  14166  rlimsqzlem  14173  lo1le  14176  climsup  14194  climcau  14195  caucvgrlem2  14199  iseralt  14209  cvgcmp  14335  cvgcmpce  14337  supcvg  14373  rpnnen2lem12  14739  bezoutlem1  15040  lcmgcdlem  15103  divgcdcoprmex  15164  exprmfct  15200  prmdvdsfz  15201  pclem  15327  pc2dvds  15367  pcprmpw  15371  dvdsprmpweqle  15374  unbenlem  15396  infpnlem2  15399  infpn2  15401  prmunb  15402  vdwlem2  15470  ramub1lem2  15515  prmdvdsprmop  15531  prmgaplem7  15545  ipodrsima  16934  grpinveu  17225  dfgrp3lem  17282  psgneu  17695  odbezout  17744  sylow2blem3  17806  nn0gsumfz  18149  ringadd2  18344  irredrmul  18476  lsmelval2  18852  lbsextlem2  18926  mptcoe1fsupp  19352  znunit  19676  scmate  20077  scmatscm  20080  scmatfo  20097  mat1scmat  20106  pmatcoe1fsupp  20267  pmatcollpwfi  20348  pmatcollpw3fi  20351  mptcoe1matfsupp  20368  pm2mp  20391  chmaidscmat  20414  cpmadugsum  20444  cpmadumatpoly  20449  chcoeffeq  20452  cayhamlem3  20453  cayhamlem4  20454  neiptopnei  20688  neitr  20736  cnpnei  20820  haust1  20908  isnrm3  20915  isreg2  20933  tgcmp  20956  hauscmplem  20961  hauscmp  20962  bwth  20965  1stcfb  21000  1stcelcls  21016  lly1stc  21051  txcmplem1  21196  txlm  21203  xkococnlem  21214  filuni  21441  filufint  21476  ufilen  21486  fclscf  21581  cnextcn  21623  ustex2sym  21772  ustex3sym  21773  utopreg  21808  isucn2  21835  ucnima  21837  ucncn  21841  neipcfilu  21852  metequiv2  22066  metrest  22080  xrsmopn  22355  mulc1cncf  22447  cncfco  22449  bndth  22496  lmmcvg  22785  cfil3i  22793  iscau4  22803  cmetcaulem  22812  iscmet3lem1  22815  caussi  22821  equivcfil  22823  equivcau  22824  caubl  22831  minveclem3b  22924  ovolgelb  22972  ovollb2lem  22980  ovolctb  22982  ovolicc2lem4  23012  ioombl1lem4  23053  dyadmax  23089  volsup2  23096  itg2monolem1  23240  c1liplem1  23480  c1lip1  23481  dvivthlem1  23492  lhop1  23498  ftc1a  23521  ftc1lem6  23525  ply1divex  23617  elply2  23673  dgrlem  23706  aacjcl  23803  aalioulem2  23809  aalioulem3  23810  aalioulem4  23811  ulmcaulem  23869  ulmcau  23870  ulmss  23872  mtest  23879  itgulm  23883  reeff1o  23922  efif1olem4  24012  rlimcnp  24409  xrlimcnp  24412  lgamucov  24481  ftalem3  24518  fta  24523  muval1  24576  dvdssqf  24581  mumullem1  24622  lgsqrmod  24794  lgsqrmodndvds  24795  pntlem3  25015  ostth  25045  tgtrisegint  25111  tgbtwndiff  25118  tgcgrxfr  25131  lnext  25180  legov2  25199  legtrd  25202  hlcgrex  25229  colperpexlem3  25342  colperpex  25343  hlpasch  25366  hpgerlem  25375  hpgtr  25378  dfcgra2  25439  acopy  25442  inagswap  25448  inaghl  25449  cgrg3col4  25452  axpasch  25539  wwlknredwwlkn0  26021  2pthfrgrarn2  26303  frgrawopreglem5  26341  usgreg2spot  26360  grpoidinvlem3  26510  grpoideu  26513  grpoinveu  26523  ubthlem1  26916  minvecolem5  26927  htthlem  26964  chscllem2  27687  nmopun  28063  lnconi  28082  rnbra  28156  sumdmdii  28464  cdj3lem2b  28486  foresf1o  28533  acunirnmpt  28647  xrofsup  28729  isarchi3  28878  isarchiofld  28954  lmxrge0  29132  lmdvg  29133  esumlub  29255  esumfsup  29265  esumcvg  29281  eulerpartlemgvv  29571  cvmliftmolem2  30324  cvmlift2lem10  30354  cvmlift2lem12  30356  frmin  30789  wzel  30821  wzelOLD  30822  wsuclem  30823  wsuclemOLD  30824  nofulllem5  30911  btwndiff  31110  trisegint  31111  cgrxfr  31138  lineext  31159  segcon2  31188  brsegle2  31192  seglecgr12im  31193  segletr  31197  broutsideof3  31209  opnrebl2  31292  nn0prpw  31294  fin2so  32369  poimirlem27  32409  poimirlem30  32412  poimirlem31  32413  poimir  32415  mblfinlem1  32419  mblfinlem2  32420  mblfinlem3  32421  mblfinlem4  32422  itg2addnclem  32434  ftc1cnnc  32457  ftc1anclem5  32462  ftc1anclem6  32463  sdclem1  32512  geomcau  32528  equivtotbnd  32550  bndss  32558  ismtybndlem  32578  heibor1lem  32581  rrncmslem  32604  rngo2  32679  prtlem15  32981  lsateln0  33103  lsat0cv  33141  eqlkr3  33209  lkrshp  33213  lshpset2N  33227  hlhgt2  33496  hlrelat2  33510  atle  33543  athgt  33563  2dim  33577  1cvratex  33580  ps-2  33585  dalem20  33800  lhpexle1lem  34114  lhpexle1  34115  lhpexle2lem  34116  lhpmcvr5N  34134  lhpmcvr6N  34135  cdleme25a  34462  cdleme29ex  34483  cdlemfnid  34673  cdlemg33b0  34810  cdlemg33a  34815  cdlemg35  34822  cdleml3N  35087  dihlsscpre  35344  dih1dimb2  35351  dihatexv  35448  dvh3dim2  35558  dochkr1  35588  dochkr1OLDN  35589  lcfl8  35612  lcfl8b  35614  lcfrlem5  35656  lcfrlem6  35657  mapdrvallem2  35755  mapdh9a  35900  mapdh9aOLDN  35901  hdmaprnlem3eN  35971  hdmaprnlem16N  35975  fphpdo  36202  rencldnfilem  36205  irrapxlem2  36208  cvgdvgrat  37337  expgrowth  37359  projf1o  38184  ssfiunibd  38267  supxrgere  38294  supxrgelem  38298  suplesup  38300  infrpge  38312  infleinf  38333  qinioo  38413  qelioo  38424  climinf  38477  mullimc  38487  islptre  38490  limccog  38491  mullimcf  38494  limcrecl  38500  sumnnodd  38501  neglimc  38518  0ellimcdiv  38520  limclner  38522  allbutfifvre  38546  climleltrp  38547  fnlimabslt  38550  cncfioobd  38587  stoweidlem7  38704  stoweidlem27  38724  stoweidlem39  38736  stoweidlem48  38745  stoweidlem49  38746  stoweidlem60  38757  stoweidlem61  38758  stoweid  38760  dirkercncflem2  38801  fourierdlem20  38824  fourierdlem39  38843  fourierdlem41  38845  fourierdlem48  38851  fourierdlem49  38852  fourierdlem50  38853  fourierdlem64  38867  fourierdlem73  38876  fourierdlem74  38877  fourierdlem75  38878  fourierdlem87  38890  fourierdlem103  38906  fourierdlem104  38907  qndenserrnopnlem  38997  sge0ltfirp  39097  sge0gerpmpt  39099  sge0ltfirpmpt2  39123  sge0isum  39124  sge0pnffigtmpt  39137  sge0pnffsumgt  39139  sge0gtfsumgt  39140  sge0uzfsumgt  39141  nnfoctbdjlem  39152  meaiuninclem  39177  omeiunltfirp  39213  carageniuncllem2  39216  hoicvr  39242  volicorescl  39247  hoidmv1le  39288  hoidmvlelem3  39291  hoiqssbllem3  39318  hspmbllem2  39321  iunhoiioolem  39370  vonioo  39377  vonicc  39380  smfaddlem1  39453  smflimlem2  39462  smflimlem3  39463  smfmullem4  39483  2pwp1prmfmtno  39847  proththd  39874  bgoldbwt  40004  bgoldbst  40005  sgoldbalt  40008  bgoldbtbndlem4  40029  bgoldbtbnd  40030  wwlksnredwwlkn0  41104  2pthfrgrrn2  41455  frgrwopreglem5  41487  zrninitoringc  41865  ply1mulgsumlem3  41972  ply1mulgsumlem4  41973  islindeps2  42068  isldepslvec2  42070
  Copyright terms: Public domain W3C validator