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

Theorem reximdva 3215
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 399 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 3213 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2157  wrex 3108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-ral 3112  df-rex 3113
This theorem is referenced by:  reximddv  3216  reximdvva  3218  reximddv2  3219  wereu2  5321  dffo4  6606  nnaordex  7964  frfi  8453  fisupg  8456  marypha1  8588  fiinfg  8653  wemapsolem  8703  unwdomg  8737  rankr1ai  8917  cofsmo  9385  cfcoflem  9388  inar1  9891  nqerf  10046  prlem936  10163  fimaxre  11262  arch  11575  bndndx  11577  suprfinzcl  11777  zmin  12022  qbtwnxr  12268  qsqueeze  12269  qextltlem  12270  xrsupsslem  12374  xrinfmsslem  12375  xrub  12379  supxrunb1  12386  ssnn0fi  13027  fsuppmapnn0fiub0  13035  fsuppmapnn0fz  13038  expnlbnd2  13237  r19.29uz  14332  cau3lem  14336  rlim2lt  14470  rlimclim  14519  2clim  14545  o1co  14559  climcn1  14564  climcn2  14565  rlimo1  14589  climsqz  14613  climsqz2  14614  rlimsqzlem  14621  lo1le  14624  climsup  14642  climcau  14643  caucvgrlem2  14647  iseralt  14657  cvgcmp  14789  cvgcmpce  14791  supcvg  14829  rpnnen2lem12  15193  bezoutlem1  15494  divgcdcoprmex  15617  exprmfct  15652  prmdvdsfz  15653  pclem  15779  pc2dvds  15819  pcprmpw  15823  dvdsprmpweqle  15826  unbenlem  15848  infpnlem2  15851  infpn2  15853  prmunb  15854  vdwlem2  15922  ramub1lem2  15967  prmdvdsprmop  15983  prmgaplem7  15997  ipodrsima  17389  grpinveu  17680  dfgrp3lem  17737  psgneu  18146  odbezout  18195  sylow2blem3  18257  nn0gsumfz  18600  ringadd2  18796  irredrmul  18928  lbsextlem2  19387  mptcoe1fsupp  19812  znunit  20138  scmate  20547  scmatscm  20550  scmatfo  20567  mat1scmat  20576  pmatcoe1fsupp  20739  pmatcollpwfi  20820  pmatcollpw3fi  20823  mptcoe1matfsupp  20840  pm2mp  20863  chmaidscmat  20886  cpmadumatpoly  20921  chcoeffeq  20924  cayhamlem3  20925  cayhamlem4  20926  neiptopnei  21170  neitr  21218  cnpnei  21302  haust1  21390  isnrm3  21397  isreg2  21415  tgcmp  21438  hauscmplem  21443  hauscmp  21444  bwth  21447  1stcfb  21482  1stcelcls  21498  lly1stc  21533  txcmplem1  21678  txlm  21685  xkococnlem  21696  filuni  21922  filufint  21957  ufilen  21967  fclscf  22062  cnextcn  22104  ustex2sym  22253  ustex3sym  22254  utopreg  22289  isucn2  22316  ucnima  22318  ucncn  22322  neipcfilu  22333  metequiv2  22548  metrest  22562  xrsmopn  22848  mulc1cncf  22941  cncfco  22943  bndth  22990  lmmcvg  23292  cfil3i  23300  iscau4  23310  cmetcaulem  23319  iscmet3lem1  23322  caussi  23328  equivcfil  23330  equivcau  23331  caubl  23339  minveclem3b  23433  ovolgelb  23483  ovollb2lem  23491  ovolctb  23493  ovolicc2lem4  23523  ioombl1lem4  23564  dyadmax  23601  volsup2  23608  itg2monolem1  23753  c1liplem1  23995  c1lip1  23996  dvivthlem1  24007  lhop1  24013  ftc1a  24036  ftc1lem6  24040  ply1divex  24132  elply2  24188  dgrlem  24221  aacjcl  24318  aalioulem2  24324  aalioulem3  24325  aalioulem4  24326  ulmcaulem  24384  ulmcau  24385  ulmss  24387  mtest  24394  itgulm  24398  reeff1o  24437  efif1olem4  24528  rlimcnp  24928  xrlimcnp  24931  lgamucov  25000  ftalem3  25037  fta  25042  muval1  25095  dvdssqf  25100  mumullem1  25141  lgsqrmod  25313  lgsqrmodndvds  25314  pntlem3  25534  ostth  25564  tgtrisegint  25630  tgbtwndiff  25637  tgcgrxfr  25649  lnext  25698  legov2  25717  legtrd  25720  hlcgrex  25747  colperpexlem3  25860  colperpex  25861  hlpasch  25884  hpgerlem  25893  hpgtr  25896  dfcgra2  25957  acopy  25960  inagswap  25966  inaghl  25967  cgrg3col4  25970  axpasch  26057  wwlksnredwwlkn0  27055  midwwlks2s3  27114  clwwlkn1loopb  27214  2pthfrgrrn2  27480  frgrwopreg1  27515  frgrwopreg2  27516  grpoidinvlem3  27711  grpoideu  27714  grpoinveu  27724  ubthlem1  28076  minvecolem5  28087  htthlem  28124  chscllem2  28847  nmopun  29223  lnconi  29242  rnbra  29316  sumdmdii  29624  cdj3lem2b  29646  foresf1o  29690  acunirnmpt  29808  xrofsup  29882  fprodex01  29920  isarchi3  30088  isarchiofld  30164  lmxrge0  30345  lmdvg  30346  esumlub  30469  esumfsup  30479  esumcvg  30495  ftc2re  31023  cvmliftmolem2  31608  cvmlift2lem12  31640  frpomin  32080  frmin  32084  wzel  32111  wsuclem  32112  nosupno  32191  nosupbnd1lem4  32199  conway  32252  btwndiff  32476  trisegint  32477  cgrxfr  32504  lineext  32525  segcon2  32554  brsegle2  32558  seglecgr12im  32559  segletr  32563  broutsideof3  32575  opnrebl2  32658  nn0prpw  32660  fin2so  33727  poimirlem27  33767  poimirlem30  33770  poimirlem31  33771  poimir  33773  mblfinlem1  33777  mblfinlem2  33778  mblfinlem3  33779  mblfinlem4  33780  itg2addnclem  33791  ftc1cnnc  33814  ftc1anclem5  33819  sdclem1  33868  geomcau  33884  equivtotbnd  33906  bndss  33914  ismtybndlem  33934  heibor1lem  33937  rrncmslem  33960  rngo2  34035  prtlem15  34672  lsateln0  34793  lsat0cv  34831  eqlkr3  34899  lkrshp  34903  lshpset2N  34917  hlhgt2  35187  hlrelat2  35201  atle  35234  athgt  35254  2dim  35268  1cvratex  35271  ps-2  35276  dalem20  35491  lhpexle1lem  35805  lhpexle1  35806  lhpexle2lem  35807  lhpmcvr5N  35825  lhpmcvr6N  35826  cdleme25a  36151  cdleme29ex  36172  cdlemfnid  36362  cdlemg33b0  36499  cdlemg33a  36504  cdlemg35  36511  cdleml3N  36776  dihlsscpre  37032  dih1dimb2  37039  dihatexv  37136  dvh3dim2  37246  dochkr1  37276  dochkr1OLDN  37277  lcfl8  37300  lcfl8b  37302  lcfrlem5  37344  lcfrlem6  37345  mapdrvallem2  37443  mapdh9a  37587  mapdh9aOLDN  37588  hdmaprnlem3eN  37656  hdmaprnlem16N  37660  fphpdo  37900  rencldnfilem  37903  irrapxlem2  37906  cvgdvgrat  39029  expgrowth  39051  projf1o  39892  rnmptlb  39954  rnmptbddlem  39956  rnmptbd2lem  39963  ssfiunibd  40021  supxrgere  40046  supxrgelem  40050  suplesup  40052  infrpge  40064  infleinf  40085  supxrunb3  40119  unb2ltle  40138  uzub  40154  qinioo  40259  qelioo  40270  climinf  40335  mullimc  40345  islptre  40348  limccog  40349  mullimcf  40352  limcrecl  40358  sumnnodd  40359  neglimc  40376  0ellimcdiv  40378  limclner  40380  allbutfifvre  40404  climleltrp  40405  fnlimabslt  40408  climinf2lem  40435  limsuppnflem  40439  limsupvaluz2  40467  supcnvlimsup  40469  limsupgtlem  40506  liminflelimsupuz  40514  liminflimsupclim  40536  cncfioobd  40607  stoweidlem7  40720  stoweidlem27  40740  stoweidlem39  40752  stoweidlem48  40761  stoweidlem49  40762  stoweidlem60  40773  stoweidlem61  40774  stoweid  40776  dirkercncflem2  40817  fourierdlem20  40840  fourierdlem39  40859  fourierdlem41  40861  fourierdlem48  40867  fourierdlem49  40868  fourierdlem50  40869  fourierdlem64  40883  fourierdlem73  40892  fourierdlem74  40893  fourierdlem75  40894  fourierdlem87  40906  fourierdlem103  40922  fourierdlem104  40923  qndenserrnopnlem  41013  sge0ltfirp  41113  sge0gerpmpt  41115  sge0ltfirpmpt2  41139  sge0isum  41140  sge0pnffigtmpt  41153  sge0pnffsumgt  41155  sge0gtfsumgt  41156  sge0uzfsumgt  41157  nnfoctbdjlem  41168  meaiuninclem  41193  meaiuninc3v  41197  omeiunltfirp  41232  carageniuncllem2  41235  hoicvr  41261  volicorescl  41266  hoidmv1le  41307  hoidmvlelem3  41310  hoiqssbllem3  41337  hspmbllem2  41340  iunhoiioolem  41388  vonioo  41395  vonicc  41398  smfaddlem1  41470  smflimlem2  41479  smflimlem3  41480  smfmullem4  41500  2pwp1prmfmtno  42096  proththd  42123  sbgoldbwt  42257  sbgoldbst  42258  sbgoldbalt  42261  bgoldbtbndlem4  42288  bgoldbtbnd  42289  zrninitoringc  42656  ply1mulgsumlem3  42761  ply1mulgsumlem4  42762  islindeps2  42857  isldepslvec2  42859
  Copyright terms: Public domain W3C validator