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

Theorem reximdva 3046
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 3044 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  reximddv  3047  reximdvva  3048  reximddv2  3049  wereu2  5140  dffo4  6415  nnaordex  7763  frfi  8246  fisupg  8249  marypha1  8381  fiinfg  8446  wemapsolem  8496  unwdomg  8530  rankr1ai  8699  cofsmo  9129  cfcoflem  9132  inar1  9635  nqerf  9790  prlem936  9907  fimaxre  11006  arch  11327  bndndx  11329  suprfinzcl  11530  zmin  11822  qbtwnxr  12069  qsqueeze  12070  qextltlem  12071  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  supxrunb1  12187  ssnn0fi  12824  fsuppmapnn0fiub0  12833  fsuppmapnn0fz  12836  expnlbnd2  13035  r19.29uz  14134  cau3lem  14138  rlim2lt  14272  rlimclim  14321  2clim  14347  o1co  14361  climcn1  14366  climcn2  14367  rlimo1  14391  climsqz  14415  climsqz2  14416  rlimsqzlem  14423  lo1le  14426  climsup  14444  climcau  14445  caucvgrlem2  14449  iseralt  14459  cvgcmp  14592  cvgcmpce  14594  supcvg  14632  rpnnen2lem12  14998  bezoutlem1  15303  divgcdcoprmex  15427  exprmfct  15463  prmdvdsfz  15464  pclem  15590  pc2dvds  15630  pcprmpw  15634  dvdsprmpweqle  15637  unbenlem  15659  infpnlem2  15662  infpn2  15664  prmunb  15665  vdwlem2  15733  ramub1lem2  15778  prmdvdsprmop  15794  prmgaplem7  15808  ipodrsima  17212  grpinveu  17503  dfgrp3lem  17560  psgneu  17972  odbezout  18021  sylow2blem3  18083  nn0gsumfz  18426  ringadd2  18621  irredrmul  18753  lbsextlem2  19207  mptcoe1fsupp  19633  znunit  19960  scmate  20364  scmatscm  20367  scmatfo  20384  mat1scmat  20393  pmatcoe1fsupp  20554  pmatcollpwfi  20635  pmatcollpw3fi  20638  mptcoe1matfsupp  20655  pm2mp  20678  chmaidscmat  20701  cpmadumatpoly  20736  chcoeffeq  20739  cayhamlem3  20740  cayhamlem4  20741  neiptopnei  20984  neitr  21032  cnpnei  21116  haust1  21204  isnrm3  21211  isreg2  21229  tgcmp  21252  hauscmplem  21257  hauscmp  21258  bwth  21261  1stcfb  21296  1stcelcls  21312  lly1stc  21347  txcmplem1  21492  txlm  21499  xkococnlem  21510  filuni  21736  filufint  21771  ufilen  21781  fclscf  21876  cnextcn  21918  ustex2sym  22067  ustex3sym  22068  utopreg  22103  isucn2  22130  ucnima  22132  ucncn  22136  neipcfilu  22147  metequiv2  22362  metrest  22376  xrsmopn  22662  mulc1cncf  22755  cncfco  22757  bndth  22804  lmmcvg  23105  cfil3i  23113  iscau4  23123  cmetcaulem  23132  iscmet3lem1  23135  caussi  23141  equivcfil  23143  equivcau  23144  caubl  23152  minveclem3b  23245  ovolgelb  23294  ovollb2lem  23302  ovolctb  23304  ovolicc2lem4  23334  ioombl1lem4  23375  dyadmax  23412  volsup2  23419  itg2monolem1  23562  c1liplem1  23804  c1lip1  23805  dvivthlem1  23816  lhop1  23822  ftc1a  23845  ftc1lem6  23849  ply1divex  23941  elply2  23997  dgrlem  24030  aacjcl  24127  aalioulem2  24133  aalioulem3  24134  aalioulem4  24135  ulmcaulem  24193  ulmcau  24194  ulmss  24196  mtest  24203  itgulm  24207  reeff1o  24246  efif1olem4  24336  rlimcnp  24737  xrlimcnp  24740  lgamucov  24809  ftalem3  24846  fta  24851  muval1  24904  dvdssqf  24909  mumullem1  24950  lgsqrmod  25122  lgsqrmodndvds  25123  pntlem3  25343  ostth  25373  tgtrisegint  25439  tgbtwndiff  25446  tgcgrxfr  25458  lnext  25507  legov2  25526  legtrd  25529  hlcgrex  25556  colperpexlem3  25669  colperpex  25670  hlpasch  25693  hpgerlem  25702  hpgtr  25705  dfcgra2  25766  acopy  25769  inagswap  25775  inaghl  25776  cgrg3col4  25779  axpasch  25866  wwlksnredwwlkn0  26859  midwwlks2s3  26917  clwwlkn1loopb  27006  2pthfrgrrn2  27263  frgrwopreg1  27298  frgrwopreg2  27299  grpoidinvlem3  27488  grpoideu  27491  grpoinveu  27501  ubthlem1  27854  minvecolem5  27865  htthlem  27902  chscllem2  28625  nmopun  29001  lnconi  29020  rnbra  29094  sumdmdii  29402  cdj3lem2b  29424  foresf1o  29469  acunirnmpt  29587  xrofsup  29661  fprodex01  29699  isarchi3  29869  isarchiofld  29945  lmxrge0  30126  lmdvg  30127  esumlub  30250  esumfsup  30260  esumcvg  30276  ftc2re  30804  cvmliftmolem2  31390  cvmlift2lem12  31422  frpomin  31863  frmin  31867  wzel  31894  wsuclem  31895  nosupno  31974  nosupbnd1lem4  31982  conway  32035  btwndiff  32259  trisegint  32260  cgrxfr  32287  lineext  32308  segcon2  32337  brsegle2  32341  seglecgr12im  32342  segletr  32346  broutsideof3  32358  opnrebl2  32441  nn0prpw  32443  fin2so  33526  poimirlem27  33566  poimirlem30  33569  poimirlem31  33570  poimir  33572  mblfinlem1  33576  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem  33591  ftc1cnnc  33614  ftc1anclem5  33619  sdclem1  33669  geomcau  33685  equivtotbnd  33707  bndss  33715  ismtybndlem  33735  heibor1lem  33738  rrncmslem  33761  rngo2  33836  prtlem15  34479  lsateln0  34600  lsat0cv  34638  eqlkr3  34706  lkrshp  34710  lshpset2N  34724  hlhgt2  34993  hlrelat2  35007  atle  35040  athgt  35060  2dim  35074  1cvratex  35077  ps-2  35082  dalem20  35297  lhpexle1lem  35611  lhpexle1  35612  lhpexle2lem  35613  lhpmcvr5N  35631  lhpmcvr6N  35632  cdleme25a  35958  cdleme29ex  35979  cdlemfnid  36169  cdlemg33b0  36306  cdlemg33a  36311  cdlemg35  36318  cdleml3N  36583  dihlsscpre  36840  dih1dimb2  36847  dihatexv  36944  dvh3dim2  37054  dochkr1  37084  dochkr1OLDN  37085  lcfl8  37108  lcfl8b  37110  lcfrlem5  37152  lcfrlem6  37153  mapdrvallem2  37251  mapdh9a  37396  mapdh9aOLDN  37397  hdmaprnlem3eN  37467  hdmaprnlem16N  37471  fphpdo  37698  rencldnfilem  37701  irrapxlem2  37704  cvgdvgrat  38829  expgrowth  38851  projf1o  39700  rnmptlb  39767  rnmptbddlem  39769  rnmptbd2lem  39777  ssfiunibd  39837  supxrgere  39862  supxrgelem  39866  suplesup  39868  infrpge  39880  infleinf  39901  supxrunb3  39936  unb2ltle  39955  uzub  39971  qinioo  40080  qelioo  40091  climinf  40156  mullimc  40166  islptre  40169  limccog  40170  mullimcf  40173  limcrecl  40179  sumnnodd  40180  neglimc  40197  0ellimcdiv  40199  limclner  40201  allbutfifvre  40225  climleltrp  40226  fnlimabslt  40229  climinf2lem  40256  limsuppnflem  40260  limsupvaluz2  40288  supcnvlimsup  40290  limsupgtlem  40327  liminflelimsupuz  40335  liminflimsupclim  40357  cncfioobd  40428  stoweidlem7  40542  stoweidlem27  40562  stoweidlem39  40574  stoweidlem48  40583  stoweidlem49  40584  stoweidlem60  40595  stoweidlem61  40596  stoweid  40598  dirkercncflem2  40639  fourierdlem20  40662  fourierdlem39  40681  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem64  40705  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem87  40728  fourierdlem103  40744  fourierdlem104  40745  qndenserrnopnlem  40835  sge0ltfirp  40935  sge0gerpmpt  40937  sge0ltfirpmpt2  40961  sge0isum  40962  sge0pnffigtmpt  40975  sge0pnffsumgt  40977  sge0gtfsumgt  40978  sge0uzfsumgt  40979  nnfoctbdjlem  40990  meaiuninclem  41015  meaiuninc3v  41019  omeiunltfirp  41054  carageniuncllem2  41057  hoicvr  41083  volicorescl  41088  hoidmv1le  41129  hoidmvlelem3  41132  hoiqssbllem3  41159  hspmbllem2  41162  iunhoiioolem  41210  vonioo  41217  vonicc  41220  smfaddlem1  41292  smflimlem2  41301  smflimlem3  41302  smfmullem4  41322  2pwp1prmfmtno  41829  proththd  41856  sbgoldbwt  41990  sbgoldbst  41991  sbgoldbalt  41994  bgoldbtbndlem4  42021  bgoldbtbnd  42022  zrninitoringc  42396  ply1mulgsumlem3  42501  ply1mulgsumlem4  42502  islindeps2  42597  isldepslvec2  42599
  Copyright terms: Public domain W3C validator