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

Theorem ralimdva 3161
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 414 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32a2d 29 . 2 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43ralimdv2 3157 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3062
This theorem is referenced by:  ralimdv  3163  ralimdvva  3198  wereu2  5631  frpomin  6295  fveqressseq  7031  f1mpt  7209  isores3  7281  caofrss  7654  caoftrn  7656  sorpssuni  7670  sorpssint  7671  onint  7726  xpord3inddlem  8087  smogt  8314  fisupg  9238  ixpfi2  9297  fissuni  9304  indexfi  9307  fiinfg  9440  wemaplem2  9488  rankonidlem  9769  ac5num  9977  acni2  9987  acndom2  9995  alephle  10029  dfac5  10069  cfsmolem  10211  isf34lem7  10320  isf34lem6  10321  fin1a2s  10355  acncc  10381  ttukeylem6  10455  fpwwe2lem7  10578  gchina  10640  inar1  10716  tskord  10721  grudomon  10758  grur1a  10760  dedekind  11323  fimaxre  12104  fiminre  12107  uzwo  12841  xrsupsslem  13232  xrinfmsslem  13233  fsuppmapnn0fiub0  13904  rexanre  15237  rexuz3  15239  rexico  15244  cau3lem  15245  limsupval2  15368  rlim2lt  15385  rlim3  15386  lo1bdd2  15412  lo1bddrp  15413  o1lo1  15425  climrlim2  15435  2clim  15460  o1co  15474  rlimcn1  15476  rlimcn3  15478  climcn1  15480  climcn2  15481  subcn2  15483  o1of2  15501  rlimo1  15505  o1rlimmul  15507  lo1add  15515  lo1mul  15516  climsqz  15529  climsqz2  15530  rlimsqzlem  15539  lo1le  15542  climbdd  15562  caucvgrlem  15563  caucvgrlem2  15565  caurcvg2  15568  iseralt  15575  cvgcmp  15706  cvgcmpce  15708  gcdcllem1  16384  absproddvds  16498  coprmprod  16542  coprmproddvdslem  16543  pcfac  16776  pockthg  16783  infpnlem1  16787  prmreclem2  16794  prmreclem3  16795  vdwlem11  16868  vdwlem13  16870  vdwnnlem3  16874  isacs2  17538  acsfn1  17546  acsfn2  17548  catpropd  17594  drsdirfi  18199  ipodrsima  18435  isacs5  18442  mrelatglb  18454  mrelatlub  18456  isgrpinv  18809  dfgrp3e  18852  issubg4  18952  gsmsymgreqlem2  19218  finodsubmsubg  19354  gexdvds  19371  gexcl3  19374  sylow2blem3  19409  cyggeninv  19665  gsummptnn0fz  19768  dprdff  19796  issubdrg  20261  acsfn1p  20280  cygznlem3  20992  mptcoe1fsupp  21602  cply1coe0bi  21687  gsummoncoe1  21691  scmatdmat  21880  mdetdiagid  21965  mdetunilem9  21985  cpmatmcllem  22083  m2cpminvid2lem  22119  decpmatmulsumfsupp  22138  pmatcollpw1lem1  22139  pmatcollpw2lem  22142  pmatcollpwfi  22147  pm2mpf1  22164  mptcoe1matfsupp  22167  mp2pm2mplem4  22174  pm2mpmhmlem1  22183  pm2mp  22190  chpdmat  22206  chpscmat  22207  cpmidpmatlem3  22237  cayhamlem4  22253  neiptopnei  22499  cncnp  22647  isnrm2  22725  isreg2  22744  2ndcdisj  22823  islly2  22851  dislly  22864  kgen2ss  22922  ptbasfi  22948  ptclsg  22982  prdstopn  22995  txtube  23007  txlm  23015  isr0  23104  filuni  23252  alexsubALTlem3  23416  ptcmplem3  23421  ptcmplem4  23422  tsmsxplem1  23520  prdsmet  23739  metequiv2  23882  metcnpi3  23918  nmoleub  24111  rescncf  24276  cncfco  24286  evth  24338  lebnumlem3  24342  xlebnum  24344  nmoleub2lem2  24495  nmhmcn  24499  lmmcvg  24641  cmetcaulem  24668  caubl  24688  bcth3  24711  ovollb2lem  24868  ovoliunlem2  24883  ovolicc2lem3  24899  ovolicc2lem4  24900  nulmbl2  24916  volsup  24936  ioombl1lem4  24941  dyadmax  24978  vitalilem2  24989  vitalilem5  24992  mbfi1flimlem  25103  itg2seq  25123  itg2addlem  25139  itgcn  25225  limciun  25274  rolle  25370  dvfsumrlim  25411  itgsubst  25429  aannenlem1  25704  aalioulem3  25710  ulmcaulem  25769  ulmcau  25770  ulmss  25772  ulmbdd  25773  ulmcn  25774  ulmdvlem3  25777  mtest  25779  iblulm  25782  itgulm  25783  rlimcnp  26331  xrlimcnp  26334  rlimcxp  26339  o1cxp  26340  amgm  26356  lgambdd  26402  ftalem2  26439  isppw2  26480  mumullem2  26545  2sqlem6  26787  chtppilimlem2  26838  chtppilim  26839  pntrsumbnd2  26931  pntlem3  26973  nosupbnd1lem5  27076  noinfbnd1lem5  27091  noetasuplem4  27100  noetainflem4  27104  isperp2  27699  axeuclidlem  27953  axeuclid  27954  uhgrnbgr0nb  28344  vtxdginducedm1fi  28534  cusgrrusgr  28571  rusgrpropnb  28573  rusgrpropedg  28574  rusgrpropadjvtx  28575  upgrewlkle2  28596  wlkvtxiedg  28615  upgrwlkvtxedg  28635  uspgr2wlkeq  28636  redwlk  28662  wlkdlem2  28673  lfgrwlkprop  28677  2pthnloop  28721  upgr2pthnlp  28722  pthdlem1  28756  pthdlem2lem  28757  wlkiswwlks1  28854  wlkiswwlks2lem4  28859  wwlksm1edg  28868  wwlksnred  28879  clwwlkccatlem  28975  clwlkclwwlklem2a  28984  clwlkclwwlklem2  28986  cusconngr  29177  eucrctshift  29229  2pthfrgr  29270  3cyclfrgr  29274  nmoub3i  29757  ubthlem1  29854  ubthlem3  29856  ocsh  30267  chintcli  30315  chscllem2  30622  nmopub2tALT  30893  nmfnleub2  30910  lnconi  31017  riesz1  31049  rnbra  31091  leopadd  31116  leopmuli  31117  leoptr  31121  dmdbr3  31289  dmdbr4  31290  dmdbr5  31292  mdsl0  31294  mdsymlem6  31392  cdj1i  31417  acunirnmpt  31621  xrge0infss  31712  elrspunidl  32251  evls1fpws  32320  cmppcmp  32496  zarclsiin  32509  lmxrge0  32590  ftc2re  33268  cvmlift2lem12  33965  opnrebl2  34839  neibastop1  34877  neibastop2lem  34878  neibastop3  34880  finixpnum  36109  lindsenlbs  36119  matunitlindflem1  36120  matunitlindflem2  36121  ptrecube  36124  poimirlem26  36150  poimirlem27  36151  poimirlem29  36153  poimirlem30  36154  poimir  36157  heicant  36159  itg2addnclem  36175  itg2addnclem3  36177  itg2addnc  36178  filbcmb  36245  nninfnub  36256  geomcau  36264  sstotbnd2  36279  isbndx  36287  prdsbnd  36298  heibor1lem  36314  heiborlem1  36316  heibor  36326  rrncmslem  36337  intidl  36534  pclclN  38400  lauteq  38604  ltrnid  38644  mapdh9a  40298  sticksstones3  40602  fltaccoprm  41021  fltabcoprm  41023  flt4lem5  41031  elrfirn2  41062  isnacs3  41076  rencldnfilem  41186  kelac1  41433  naddgeoa  41754  neik0pk1imk0  42407  cvgdvgrat  42681  neglimc  43974  limsupub  44031  limsuppnflem  44037  limsupre3lem  44059  limsupvaluz2  44065  supcnvlimsup  44067  climuzlem  44070  liminfval2  44095  limsupgtlem  44104  liminflelimsupuz  44112  liminflimsupclim  44134  xlimpnfxnegmnf  44141  liminflimsupxrre  44144  xlimmnfv  44161  xlimpnfv  44165  stoweidlem7  44334  fourierdlem73  44506  sge0isum  44754  meaiuninc3v  44811  preimageiingt  45047  preimaleiinlt  45048  smflimlem3  45100  smflimlem4  45101  cfsetsnfsetfo  45380  2reu8i  45431  iccpartres  45696  upwlkwlk  46127  upgrwlkupwlk  46128  copisnmnd  46189  2zrngnmlid2  46335  ply1mulgsumlem1  46553  ply1mulgsumlem3  46555  ply1mulgsumlem4  46556  snlindsntor  46638  eenglngeehlnmlem1  46909  eenglngeehlnmlem2  46910
  Copyright terms: Public domain W3C validator