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

Theorem ralimdva 3150
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
Hypothesis
Ref Expression
ralimdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralimdva (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdva
StepHypRef Expression
1 ralimdva.1 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 399 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32a2d 29 . 2 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43ralimdv2 3149 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2156  wral 3096
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-ral 3101
This theorem is referenced by:  ralimdv  3151  ralimdvva  3152  wereu2  5308  fveqressseq  6573  f1mpt  6738  isores3  6805  caofrss  7156  caoftrn  7158  sorpssuni  7172  sorpssint  7173  onint  7221  smogt  7696  fisupg  8443  ixpfi2  8499  fissuni  8506  indexfi  8509  fiinfg  8640  wemaplem2  8687  rankonidlem  8934  ac5num  9138  acni2  9148  acndom2  9156  alephle  9190  dfac5  9230  cfsmolem  9373  isf34lem7  9482  isf34lem6  9483  fin1a2s  9517  acncc  9543  ttukeylem6  9617  fpwwe2lem8  9740  gchina  9802  inar1  9878  tskord  9883  grudomon  9920  grur1a  9922  dedekind  10481  fimaxre  11249  uzwo  11966  xrsupsslem  12351  xrinfmsslem  12352  fsuppmapnn0fiub0  13012  rexanre  14305  rexuz3  14307  rexico  14312  cau3lem  14313  limsupval2  14430  rlim2lt  14447  rlim3  14448  lo1bdd2  14474  lo1bddrp  14475  o1lo1  14487  climrlim2  14497  2clim  14522  o1co  14536  rlimcn1  14538  rlimcn2  14540  climcn1  14541  climcn2  14542  subcn2  14544  o1of2  14562  rlimo1  14566  o1rlimmul  14568  lo1add  14576  lo1mul  14577  climsqz  14590  climsqz2  14591  rlimsqzlem  14598  lo1le  14601  climbdd  14621  caucvgrlem  14622  caucvgrlem2  14624  caurcvg2  14627  iseralt  14634  cvgcmp  14766  cvgcmpce  14768  gcdcllem1  15436  absproddvds  15545  coprmprod  15589  coprmproddvdslem  15590  pcfac  15816  pockthg  15823  infpnlem1  15827  prmreclem2  15834  prmreclem3  15835  vdwlem11  15908  vdwlem13  15910  vdwnnlem3  15914  isacs2  16514  acsfn1  16522  acsfn2  16524  catpropd  16569  drsdirfi  17139  ipodrsima  17366  isacs5  17373  mrelatglb  17385  mrelatlub  17387  isgrpinv  17673  dfgrp3e  17716  issubg4  17811  gsmsymgreqlem2  18048  gexdvds  18196  gexcl3  18199  sylow2blem3  18234  cyggeninv  18482  gsummptnn0fz  18579  gsummptnn0fzOLD  18580  dprdff  18609  issubdrg  19005  mptcoe1fsupp  19789  cply1coe0bi  19874  gsummoncoe1  19878  cygznlem3  20121  scmatdmat  20529  mdetdiagid  20614  mdetunilem9  20634  cpmatmcllem  20733  m2cpminvid2lem  20769  decpmatmulsumfsupp  20788  pmatcollpw1lem1  20789  pmatcollpw2lem  20792  pmatcollpwfi  20797  pm2mpf1  20814  mptcoe1matfsupp  20817  mp2pm2mplem4  20824  pm2mpmhmlem1  20833  pm2mp  20840  chpdmat  20856  chpscmat  20857  cpmidpmatlem3  20887  cayhamlem4  20903  neiptopnei  21147  cncnp  21295  isnrm2  21373  isreg2  21392  2ndcdisj  21470  islly2  21498  dislly  21511  kgen2ss  21569  ptbasfi  21595  ptclsg  21629  prdstopn  21642  txtube  21654  txlm  21662  isr0  21751  filuni  21899  alexsubALTlem3  22063  ptcmplem3  22068  ptcmplem4  22069  tsmsxplem1  22166  prdsmet  22385  metequiv2  22525  metcnpi3  22561  nmoleub  22745  rescncf  22910  cncfco  22920  evth  22968  lebnumlem3  22972  xlebnum  22974  nmoleub2lem2  23125  nmhmcn  23129  lmmcvg  23269  cmetcaulem  23296  caubl  23316  bcth3  23338  ovollb2lem  23468  ovoliunlem2  23483  ovolicc2lem3  23499  ovolicc2lem4  23500  nulmbl2  23516  volsup  23536  ioombl1lem4  23541  dyadmax  23578  vitalilem2  23589  vitalilem5  23592  mbfi1flimlem  23702  itg2seq  23722  itg2addlem  23738  itgcn  23822  limciun  23871  rolle  23966  dvfsumrlim  24007  itgsubst  24025  aannenlem1  24296  aalioulem3  24302  ulmcaulem  24361  ulmcau  24362  ulmss  24364  ulmbdd  24365  ulmcn  24366  ulmdvlem3  24369  mtest  24371  iblulm  24374  itgulm  24375  rlimcnp  24905  xrlimcnp  24908  rlimcxp  24913  o1cxp  24914  amgm  24930  lgambdd  24976  ftalem2  25013  isppw2  25054  mumullem2  25119  2sqlem6  25361  chtppilimlem2  25376  chtppilim  25377  pntrsumbnd2  25469  pntlem3  25511  isperp2  25823  axeuclidlem  26055  axeuclid  26056  uhgrnbgr0nb  26465  vtxdginducedm1fi  26667  cusgrrusgr  26704  rusgrpropnb  26706  rusgrpropedg  26707  rusgrpropadjvtx  26708  upgrewlkle2  26729  wlkvtxiedg  26747  upgrwlkvtxedg  26768  uspgr2wlkeq  26769  redwlk  26796  wlkdlem2  26807  lfgrwlkprop  26811  2pthnloop  26854  upgr2pthnlp  26855  pthdlem1  26889  pthdlem2lem  26890  wlkiswwlks1  26993  wlkiswwlks2lem4  26998  wwlksm1edg  27007  wwlksnred  27028  clwwlkccatlem  27131  clwlkclwwlklem2a  27140  clwlkclwwlklem2  27142  cusconngr  27363  eucrctshift  27415  2pthfrgr  27458  3cyclfrgr  27462  nmoub3i  27955  ubthlem1  28053  ubthlem3  28055  ocsh  28469  chintcli  28517  chscllem2  28824  nmopub2tALT  29095  nmfnleub2  29112  lnconi  29219  riesz1  29251  rnbra  29293  leopadd  29318  leopmuli  29319  leoptr  29323  dmdbr3  29491  dmdbr4  29492  dmdbr5  29494  mdsl0  29496  mdsymlem6  29594  cdj1i  29619  acunirnmpt  29785  xrge0infss  29851  cmppcmp  30249  lmxrge0  30322  ftc2re  31000  cvmlift2lem12  31617  frpomin  32057  nosupbnd1lem5  32177  noetalem3  32184  opnrebl2  32635  neibastop1  32673  neibastop2lem  32674  neibastop3  32676  finixpnum  33705  lindsenlbs  33715  matunitlindflem1  33716  matunitlindflem2  33717  ptrecube  33720  poimirlem26  33746  poimirlem27  33747  poimirlem29  33749  poimirlem30  33750  poimir  33753  heicant  33755  itg2addnclem  33771  itg2addnclem3  33773  itg2addnc  33774  filbcmb  33845  nninfnub  33856  geomcau  33864  sstotbnd2  33882  isbndx  33890  prdsbnd  33901  heibor1lem  33917  heiborlem1  33919  heibor  33929  rrncmslem  33940  intidl  34137  pclclN  35669  lauteq  35873  ltrnid  35913  mapdh9a  37567  elrfirn2  37758  isnacs3  37772  rencldnfilem  37883  kelac1  38131  acsfn1p  38267  neik0pk1imk0  38842  cvgdvgrat  39009  neglimc  40356  limsupub  40413  limsuppnflem  40419  limsupre3lem  40441  limsupvaluz2  40447  supcnvlimsup  40449  climuzlem  40452  liminfval2  40477  limsupgtlem  40486  liminflelimsupuz  40494  liminflimsupclim  40516  xlimmnfv  40537  xlimpnfv  40541  stoweidlem7  40700  fourierdlem73  40872  sge0isum  41120  meaiuninc3v  41177  preimageiingt  41409  preimaleiinlt  41410  smflimlem3  41460  smflimlem4  41461  iccpartres  41926  upwlkwlk  42285  upgrwlkupwlk  42286  copisnmnd  42374  2zrngnmlid2  42516  ply1mulgsumlem1  42739  ply1mulgsumlem3  42741  ply1mulgsumlem4  42742  snlindsntor  42825
  Copyright terms: Public domain W3C validator