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

Theorem reximdva 3000
 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 449 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 2998 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902 This theorem is referenced by:  reximddv  3001  reximddv2  3002  wereu2  5035  dffo4  6283  nnaordex  7605  frfi  8090  fisupg  8093  marypha1  8223  fiinfg  8288  wemapsolem  8338  unwdomg  8372  rankr1ai  8544  cofsmo  8974  cfcoflem  8977  inar1  9476  nqerf  9631  prlem936  9748  fimaxre  10847  arch  11166  bndndx  11168  suprfinzcl  11368  zmin  11660  qbtwnxr  11905  qsqueeze  11906  qextltlem  11907  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  supxrunb1  12021  ssnn0fi  12646  fsuppmapnn0fiub0  12655  fsuppmapnn0fz  12658  expnlbnd2  12857  r19.29uz  13938  cau3lem  13942  rlim2lt  14076  rlimclim  14125  2clim  14151  o1co  14165  climcn1  14170  climcn2  14171  rlimo1  14195  climsqz  14219  climsqz2  14220  rlimsqzlem  14227  lo1le  14230  climsup  14248  climcau  14249  caucvgrlem2  14253  iseralt  14263  cvgcmp  14389  cvgcmpce  14391  supcvg  14427  rpnnen2lem12  14793  bezoutlem1  15094  lcmgcdlem  15157  divgcdcoprmex  15218  exprmfct  15254  prmdvdsfz  15255  pclem  15381  pc2dvds  15421  pcprmpw  15425  dvdsprmpweqle  15428  unbenlem  15450  infpnlem2  15453  infpn2  15455  prmunb  15456  vdwlem2  15524  ramub1lem2  15569  prmdvdsprmop  15585  prmgaplem7  15599  ipodrsima  16988  grpinveu  17279  dfgrp3lem  17336  psgneu  17749  odbezout  17798  sylow2blem3  17860  nn0gsumfz  18203  ringadd2  18398  irredrmul  18530  lsmelval2  18906  lbsextlem2  18980  mptcoe1fsupp  19406  znunit  19731  scmate  20135  scmatscm  20138  scmatfo  20155  mat1scmat  20164  pmatcoe1fsupp  20325  pmatcollpwfi  20406  pmatcollpw3fi  20409  mptcoe1matfsupp  20426  pm2mp  20449  chmaidscmat  20472  cpmadugsum  20502  cpmadumatpoly  20507  chcoeffeq  20510  cayhamlem3  20511  cayhamlem4  20512  neiptopnei  20746  neitr  20794  cnpnei  20878  haust1  20966  isnrm3  20973  isreg2  20991  tgcmp  21014  hauscmplem  21019  hauscmp  21020  bwth  21023  1stcfb  21058  1stcelcls  21074  lly1stc  21109  txcmplem1  21254  txlm  21261  xkococnlem  21272  filuni  21499  filufint  21534  ufilen  21544  fclscf  21639  cnextcn  21681  ustex2sym  21830  ustex3sym  21831  utopreg  21866  isucn2  21893  ucnima  21895  ucncn  21899  neipcfilu  21910  metequiv2  22125  metrest  22139  xrsmopn  22423  mulc1cncf  22516  cncfco  22518  bndth  22565  lmmcvg  22867  cfil3i  22875  iscau4  22885  cmetcaulem  22894  iscmet3lem1  22897  caussi  22903  equivcfil  22905  equivcau  22906  caubl  22914  minveclem3b  23007  ovolgelb  23055  ovollb2lem  23063  ovolctb  23065  ovolicc2lem4  23095  ioombl1lem4  23136  dyadmax  23172  volsup2  23179  itg2monolem1  23323  c1liplem1  23563  c1lip1  23564  dvivthlem1  23575  lhop1  23581  ftc1a  23604  ftc1lem6  23608  ply1divex  23700  elply2  23756  dgrlem  23789  aacjcl  23886  aalioulem2  23892  aalioulem3  23893  aalioulem4  23894  ulmcaulem  23952  ulmcau  23953  ulmss  23955  mtest  23962  itgulm  23966  reeff1o  24005  efif1olem4  24095  rlimcnp  24492  xrlimcnp  24495  lgamucov  24564  ftalem3  24601  fta  24606  muval1  24659  dvdssqf  24664  mumullem1  24705  lgsqrmod  24877  lgsqrmodndvds  24878  pntlem3  25098  ostth  25128  tgtrisegint  25194  tgbtwndiff  25201  tgcgrxfr  25213  lnext  25262  legov2  25281  legtrd  25284  hlcgrex  25311  colperpexlem3  25424  colperpex  25425  hlpasch  25448  hpgerlem  25457  hpgtr  25460  dfcgra2  25521  acopy  25524  inagswap  25530  inaghl  25531  cgrg3col4  25534  axpasch  25621  wwlknredwwlkn0  26255  2pthfrgrarn2  26537  frgrawopreglem5  26575  usgreg2spot  26594  grpoidinvlem3  26744  grpoideu  26747  grpoinveu  26757  ubthlem1  27110  minvecolem5  27121  htthlem  27158  chscllem2  27881  nmopun  28257  lnconi  28276  rnbra  28350  sumdmdii  28658  cdj3lem2b  28680  foresf1o  28727  acunirnmpt  28841  xrofsup  28923  isarchi3  29072  isarchiofld  29148  lmxrge0  29326  lmdvg  29327  esumlub  29449  esumfsup  29459  esumcvg  29475  eulerpartlemgvv  29765  cvmliftmolem2  30518  cvmlift2lem10  30548  cvmlift2lem12  30550  frmin  30983  wzel  31015  wzelOLD  31016  wsuclem  31017  wsuclemOLD  31018  nofulllem5  31105  btwndiff  31304  trisegint  31305  cgrxfr  31332  lineext  31353  segcon2  31382  brsegle2  31386  seglecgr12im  31387  segletr  31391  broutsideof3  31403  opnrebl2  31486  nn0prpw  31488  fin2so  32566  poimirlem27  32606  poimirlem30  32609  poimirlem31  32610  poimir  32612  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem  32631  ftc1cnnc  32654  ftc1anclem5  32659  ftc1anclem6  32660  sdclem1  32709  geomcau  32725  equivtotbnd  32747  bndss  32755  ismtybndlem  32775  heibor1lem  32778  rrncmslem  32801  rngo2  32876  prtlem15  33178  lsateln0  33300  lsat0cv  33338  eqlkr3  33406  lkrshp  33410  lshpset2N  33424  hlhgt2  33693  hlrelat2  33707  atle  33740  athgt  33760  2dim  33774  1cvratex  33777  ps-2  33782  dalem20  33997  lhpexle1lem  34311  lhpexle1  34312  lhpexle2lem  34313  lhpmcvr5N  34331  lhpmcvr6N  34332  cdleme25a  34659  cdleme29ex  34680  cdlemfnid  34870  cdlemg33b0  35007  cdlemg33a  35012  cdlemg35  35019  cdleml3N  35284  dihlsscpre  35541  dih1dimb2  35548  dihatexv  35645  dvh3dim2  35755  dochkr1  35785  dochkr1OLDN  35786  lcfl8  35809  lcfl8b  35811  lcfrlem5  35853  lcfrlem6  35854  mapdrvallem2  35952  mapdh9a  36097  mapdh9aOLDN  36098  hdmaprnlem3eN  36168  hdmaprnlem16N  36172  fphpdo  36399  rencldnfilem  36402  irrapxlem2  36405  cvgdvgrat  37534  expgrowth  37556  projf1o  38381  ssfiunibd  38464  supxrgere  38490  supxrgelem  38494  suplesup  38496  infrpge  38508  infleinf  38529  qinioo  38609  qelioo  38620  climinf  38673  mullimc  38683  islptre  38686  limccog  38687  mullimcf  38690  limcrecl  38696  sumnnodd  38697  neglimc  38714  0ellimcdiv  38716  limclner  38718  allbutfifvre  38742  climleltrp  38743  fnlimabslt  38746  cncfioobd  38783  stoweidlem7  38900  stoweidlem27  38920  stoweidlem39  38932  stoweidlem48  38941  stoweidlem49  38942  stoweidlem60  38953  stoweidlem61  38954  stoweid  38956  dirkercncflem2  38997  fourierdlem20  39020  fourierdlem39  39039  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem64  39063  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  qndenserrnopnlem  39193  sge0ltfirp  39293  sge0gerpmpt  39295  sge0ltfirpmpt2  39319  sge0isum  39320  sge0pnffigtmpt  39333  sge0pnffsumgt  39335  sge0gtfsumgt  39336  sge0uzfsumgt  39337  nnfoctbdjlem  39348  meaiuninclem  39373  omeiunltfirp  39409  carageniuncllem2  39412  hoicvr  39438  volicorescl  39443  hoidmv1le  39484  hoidmvlelem3  39487  hoiqssbllem3  39514  hspmbllem2  39517  iunhoiioolem  39566  vonioo  39573  vonicc  39576  smfaddlem1  39649  smflimlem2  39658  smflimlem3  39659  smfmullem4  39679  2pwp1prmfmtno  40042  proththd  40069  bgoldbwt  40199  bgoldbst  40200  sgoldbalt  40203  bgoldbtbndlem4  40224  bgoldbtbnd  40225  wwlksnredwwlkn0  41102  2pthfrgrrn2  41453  frgrwopreglem5  41485  zrninitoringc  41863  ply1mulgsumlem3  41970  ply1mulgsumlem4  41971  islindeps2  42066  isldepslvec2  42068
 Copyright terms: Public domain W3C validator