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

Theorem reximdva 3013
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 450 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 3011 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2913  df-rex 2914
This theorem is referenced by:  reximddv  3014  reximddv2  3015  wereu2  5081  dffo4  6341  nnaordex  7678  frfi  8165  fisupg  8168  marypha1  8300  fiinfg  8365  wemapsolem  8415  unwdomg  8449  rankr1ai  8621  cofsmo  9051  cfcoflem  9054  inar1  9557  nqerf  9712  prlem936  9829  fimaxre  10928  arch  11249  bndndx  11251  suprfinzcl  11452  zmin  11744  qbtwnxr  11990  qsqueeze  11991  qextltlem  11992  xrsupsslem  12096  xrinfmsslem  12097  xrub  12101  supxrunb1  12108  ssnn0fi  12740  fsuppmapnn0fiub0  12749  fsuppmapnn0fz  12752  expnlbnd2  12951  r19.29uz  14040  cau3lem  14044  rlim2lt  14178  rlimclim  14227  2clim  14253  o1co  14267  climcn1  14272  climcn2  14273  rlimo1  14297  climsqz  14321  climsqz2  14322  rlimsqzlem  14329  lo1le  14332  climsup  14350  climcau  14351  caucvgrlem2  14355  iseralt  14365  cvgcmp  14494  cvgcmpce  14496  supcvg  14532  rpnnen2lem12  14898  bezoutlem1  15199  lcmgcdlem  15262  divgcdcoprmex  15323  exprmfct  15359  prmdvdsfz  15360  pclem  15486  pc2dvds  15526  pcprmpw  15530  dvdsprmpweqle  15533  unbenlem  15555  infpnlem2  15558  infpn2  15560  prmunb  15561  vdwlem2  15629  ramub1lem2  15674  prmdvdsprmop  15690  prmgaplem7  15704  ipodrsima  17105  grpinveu  17396  dfgrp3lem  17453  psgneu  17866  odbezout  17915  sylow2blem3  17977  nn0gsumfz  18320  ringadd2  18515  irredrmul  18647  lsmelval2  19025  lbsextlem2  19099  mptcoe1fsupp  19525  znunit  19852  scmate  20256  scmatscm  20259  scmatfo  20276  mat1scmat  20285  pmatcoe1fsupp  20446  pmatcollpwfi  20527  pmatcollpw3fi  20530  mptcoe1matfsupp  20547  pm2mp  20570  chmaidscmat  20593  cpmadugsum  20623  cpmadumatpoly  20628  chcoeffeq  20631  cayhamlem3  20632  cayhamlem4  20633  neiptopnei  20876  neitr  20924  cnpnei  21008  haust1  21096  isnrm3  21103  isreg2  21121  tgcmp  21144  hauscmplem  21149  hauscmp  21150  bwth  21153  1stcfb  21188  1stcelcls  21204  lly1stc  21239  txcmplem1  21384  txlm  21391  xkococnlem  21402  filuni  21629  filufint  21664  ufilen  21674  fclscf  21769  cnextcn  21811  ustex2sym  21960  ustex3sym  21961  utopreg  21996  isucn2  22023  ucnima  22025  ucncn  22029  neipcfilu  22040  metequiv2  22255  metrest  22269  xrsmopn  22555  mulc1cncf  22648  cncfco  22650  bndth  22697  lmmcvg  22999  cfil3i  23007  iscau4  23017  cmetcaulem  23026  iscmet3lem1  23029  caussi  23035  equivcfil  23037  equivcau  23038  caubl  23046  minveclem3b  23139  ovolgelb  23188  ovollb2lem  23196  ovolctb  23198  ovolicc2lem4  23228  ioombl1lem4  23269  dyadmax  23306  volsup2  23313  itg2monolem1  23457  c1liplem1  23697  c1lip1  23698  dvivthlem1  23709  lhop1  23715  ftc1a  23738  ftc1lem6  23742  ply1divex  23834  elply2  23890  dgrlem  23923  aacjcl  24020  aalioulem2  24026  aalioulem3  24027  aalioulem4  24028  ulmcaulem  24086  ulmcau  24087  ulmss  24089  mtest  24096  itgulm  24100  reeff1o  24139  efif1olem4  24229  rlimcnp  24626  xrlimcnp  24629  lgamucov  24698  ftalem3  24735  fta  24740  muval1  24793  dvdssqf  24798  mumullem1  24839  lgsqrmod  25011  lgsqrmodndvds  25012  pntlem3  25232  ostth  25262  tgtrisegint  25328  tgbtwndiff  25335  tgcgrxfr  25347  lnext  25396  legov2  25415  legtrd  25418  hlcgrex  25445  colperpexlem3  25558  colperpex  25559  hlpasch  25582  hpgerlem  25591  hpgtr  25594  dfcgra2  25655  acopy  25658  inagswap  25664  inaghl  25665  cgrg3col4  25668  axpasch  25755  wwlksnredwwlkn0  26694  2pthfrgrrn2  27045  frgrwopreglem5  27077  grpoidinvlem3  27248  grpoideu  27251  grpoinveu  27261  ubthlem1  27614  minvecolem5  27625  htthlem  27662  chscllem2  28385  nmopun  28761  lnconi  28780  rnbra  28854  sumdmdii  29162  cdj3lem2b  29184  foresf1o  29231  acunirnmpt  29342  xrofsup  29418  isarchi3  29568  isarchiofld  29644  lmxrge0  29822  lmdvg  29823  esumlub  29945  esumfsup  29955  esumcvg  29971  eulerpartlemgvv  30261  ftc2re  30492  cvmliftmolem2  31025  cvmlift2lem10  31055  cvmlift2lem12  31057  frmin  31493  wzel  31525  wzelOLD  31526  wsuclem  31527  wsuclemOLD  31528  nosino  31628  btwndiff  31829  trisegint  31830  cgrxfr  31857  lineext  31878  segcon2  31907  brsegle2  31911  seglecgr12im  31912  segletr  31916  broutsideof3  31928  opnrebl2  32011  nn0prpw  32013  fin2so  33067  poimirlem27  33107  poimirlem30  33110  poimirlem31  33111  poimir  33113  mblfinlem1  33117  mblfinlem2  33118  mblfinlem3  33119  mblfinlem4  33120  itg2addnclem  33132  ftc1cnnc  33155  ftc1anclem5  33160  ftc1anclem6  33161  sdclem1  33210  geomcau  33226  equivtotbnd  33248  bndss  33256  ismtybndlem  33276  heibor1lem  33279  rrncmslem  33302  rngo2  33377  prtlem15  33679  lsateln0  33801  lsat0cv  33839  eqlkr3  33907  lkrshp  33911  lshpset2N  33925  hlhgt2  34194  hlrelat2  34208  atle  34241  athgt  34261  2dim  34275  1cvratex  34278  ps-2  34283  dalem20  34498  lhpexle1lem  34812  lhpexle1  34813  lhpexle2lem  34814  lhpmcvr5N  34832  lhpmcvr6N  34833  cdleme25a  35160  cdleme29ex  35181  cdlemfnid  35371  cdlemg33b0  35508  cdlemg33a  35513  cdlemg35  35520  cdleml3N  35785  dihlsscpre  36042  dih1dimb2  36049  dihatexv  36146  dvh3dim2  36256  dochkr1  36286  dochkr1OLDN  36287  lcfl8  36310  lcfl8b  36312  lcfrlem5  36354  lcfrlem6  36355  mapdrvallem2  36453  mapdh9a  36598  mapdh9aOLDN  36599  hdmaprnlem3eN  36669  hdmaprnlem16N  36673  fphpdo  36900  rencldnfilem  36903  irrapxlem2  36906  cvgdvgrat  38033  expgrowth  38055  projf1o  38895  rnmptlb  38963  rnmptbddlem  38965  rnmptbd2lem  38974  ssfiunibd  39022  supxrgere  39048  supxrgelem  39052  suplesup  39054  infrpge  39066  infleinf  39087  supxrunb3  39122  unb2ltle  39141  uzub  39157  qinioo  39208  qelioo  39219  climinf  39274  mullimc  39284  islptre  39287  limccog  39288  mullimcf  39291  limcrecl  39297  sumnnodd  39298  neglimc  39315  0ellimcdiv  39317  limclner  39319  allbutfifvre  39343  climleltrp  39344  fnlimabslt  39347  climinf2lem  39374  limsuppnflem  39378  limsupvaluz2  39406  supcnvlimsup  39408  cncfioobd  39445  stoweidlem7  39561  stoweidlem27  39581  stoweidlem39  39593  stoweidlem48  39602  stoweidlem49  39603  stoweidlem60  39614  stoweidlem61  39615  stoweid  39617  dirkercncflem2  39658  fourierdlem20  39681  fourierdlem39  39700  fourierdlem41  39702  fourierdlem48  39708  fourierdlem49  39709  fourierdlem50  39710  fourierdlem64  39724  fourierdlem73  39733  fourierdlem74  39734  fourierdlem75  39735  fourierdlem87  39747  fourierdlem103  39763  fourierdlem104  39764  qndenserrnopnlem  39854  sge0ltfirp  39954  sge0gerpmpt  39956  sge0ltfirpmpt2  39980  sge0isum  39981  sge0pnffigtmpt  39994  sge0pnffsumgt  39996  sge0gtfsumgt  39997  sge0uzfsumgt  39998  nnfoctbdjlem  40009  meaiuninclem  40034  omeiunltfirp  40070  carageniuncllem2  40073  hoicvr  40099  volicorescl  40104  hoidmv1le  40145  hoidmvlelem3  40148  hoiqssbllem3  40175  hspmbllem2  40178  iunhoiioolem  40226  vonioo  40233  vonicc  40236  smfaddlem1  40308  smflimlem2  40317  smflimlem3  40318  smfmullem4  40338  2pwp1prmfmtno  40833  proththd  40860  bgoldbwt  40990  bgoldbst  40991  sgoldbalt  40994  bgoldbtbndlem4  41015  bgoldbtbnd  41016  zrninitoringc  41389  ply1mulgsumlem3  41494  ply1mulgsumlem4  41495  islindeps2  41590  isldepslvec2  41592
  Copyright terms: Public domain W3C validator