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

Theorem ralimi 2981
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1 (𝜑𝜓)
Assertion
Ref Expression
ralimi (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 2979 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  2ralimi  2982  r19.26  3093  r19.29  3101  rr19.3v  3377  rr19.28v  3378  reu3  3429  uniiunlem  3724  reupick2  3946  uniss2  4502  ss2iun  4568  iineq2  4570  iunss2  4597  disjss2  4655  disjeq2  4656  reusv2lem5  4903  issref  5544  dmmptg  5670  wfisg  5753  fununi  6002  fnmptf  6054  fnmpt  6058  mpteqb  6338  chfnrn  6368  fvn0ssdmfun  6390  dffo5  6416  ffvresb  6434  fmptcof  6437  mpt22eqb  6811  ralrnmpt2  6817  abnexg  7006  tfis  7096  fun11uni  7162  fun11iun  7168  zfrep6  7176  mpt2exxg  7289  el2mpt2csbcl  7295  frxp  7332  smores  7494  riiner  7863  ixpn0  7982  boxriin  7992  unifi2  8297  wemaplem2  8493  rankonidlem  8729  acni3  8908  dfac5  8989  dfac12lem2  9004  kmlem6  9015  kmlem8  9017  kmlem13  9022  cfsmolem  9130  fin23lem40  9211  isf32lem2  9214  fin1a2s  9274  hsmexlem2  9287  hsmex3  9294  axcc4  9299  domtriomlem  9302  dcomex  9307  ac6num  9339  iundom  9402  unirnfdomd  9427  konigthlem  9428  iunctb  9434  gch3  9536  wununi  9566  wunpw  9567  wunpr  9569  eltsk2g  9611  tskpwss  9612  tskpw  9613  grupw  9655  gruurn  9658  intgru  9674  grothpw  9686  grothpwex  9687  grothomex  9689  axgroth3  9691  suplem1pr  9912  supexpr  9914  supsr  9971  fimaxre3  11008  xrsupexmnf  12173  xrinfmexpnf  12174  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  fsuppmapnn0fiubex  12832  mptnn0fsuppd  12838  rexanre  14130  rexuz3  14132  cau3lem  14138  caubnd2  14141  caubnd  14142  rlim0  14283  rlim0lt  14284  climi2  14286  climi0  14287  climrlim2  14322  rlimres  14333  o1rlimmul  14393  caurcvg  14451  caurcvg2  14452  caucvg  14453  caucvgb  14454  sumeq2  14468  prodeq2  14688  ndvdssub  15180  gcdcllem1  15268  coprmproddvdslem  15423  vdwnnlem1  15746  imasaddfnlem  16235  catidex  16382  catlid  16391  catrid  16392  catcocl  16393  catpropd  16416  subcidcl  16551  funcid  16577  setcepi  16785  tsrss  17270  mgmidmo  17306  gsumval2  17327  isnmnd  17345  issubg2  17656  gagrpid  17773  gaass  17776  dprdcntz  18453  dprddisj  18454  abveq0  18874  abvmul  18877  abvtri  18878  psgndiflemB  19994  phllmhm  20025  ipcj  20027  ipeq0  20031  mdetmul  20477  pmatcollpw2lem  20630  eltg2b  20811  iincld  20891  iuncld  20897  isclo2  20940  neips  20965  neipeltop  20981  lmcvg  21114  t1t0  21200  hauscmplem  21257  bwth  21261  1stcelcls  21312  ptuni2  21427  pttopon  21447  ptcld  21464  ptcnplem  21472  txtube  21491  txlm  21499  xkococnlem  21510  fbun  21691  isfil2  21707  ptcmplem4  21906  ustssel  22056  isucn2  22130  ucncn  22136  metrest  22376  tngngp  22505  tngngp3  22507  ncvsi  22997  iscau4  23123  cmetcaulem  23132  caussi  23141  volfiniun  23361  iunmbl  23367  voliun  23368  mbfdm  23440  itg2seq  23554  itg2i1fseqle  23566  itg2i1fseq2  23568  iblcnlem  23600  limcresi  23694  limciun  23703  rolle  23798  ulmss  24196  rlimcnp  24737  colinearalg  25835  axpasch  25866  axeuclid  25888  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  fusgrregdegfi  26521  0grrgr  26532  rusgr1vtxlem  26539  wlkvtxeledg  26575  wlkdlem3  26637  wlkdlem4  26638  lfgriswlk  26641  lfgrwlknloop  26642  eulercrct  27220  1to3vfriendship  27261  frgrregorufr0  27304  isgrpo  27479  grpoidinv  27490  grpoideu  27491  grpoidval  27495  grpoidinv2  27497  vcidOLD  27547  vcdi  27548  vcdir  27549  vcass  27550  nvs  27646  nvz  27652  nvtri  27653  mdbr3  29284  mdbr4  29285  mdsl1i  29308  dmdbr6ati  29410  dmdbr7ati  29411  disjunsn  29533  hasheuni  30275  sigaclcu2  30311  prsiga  30322  measvunilem  30403  cntmeas  30417  omssubadd  30490  signsply0  30756  bnj1498  31255  cvmsdisj  31378  cvmshmeo  31379  cvmliftlem15  31406  cvmlift2lem12  31422  untangtr  31717  elpotr  31810  dfon2lem7  31818  dfon2lem8  31819  tfisg  31840  frpoinsg  31866  frinsg  31870  poseq  31878  opnrebl2  32441  fnemeet2  32487  fnejoin1  32488  fnejoin2  32489  dfgcd3  33300  ptrecube  33539  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  heicant  33574  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  frinfm  33660  caushft  33687  sstotbnd3  33705  prdstotbnd  33723  heibor1lem  33738  bfplem2  33752  opidonOLD  33781  exidu1  33785  grpomndo  33804  rngoideu  33832  rngodi  33833  rngodir  33834  rngoass  33835  rngoueqz  33869  idladdcl  33948  idllmulcl  33949  idlrmulcl  33950  mpt2bi123f  34101  iineq12f  34103  mptbi12f  34105  pmapglbx  35373  ltrnnid  35740  cdlemefrs32fva  36005  lerabdioph  37686  ltrabdioph  37689  nerabdioph  37690  dvdsrabdioph  37691  rencldnfi  37702  dford3  37912  pwelg  38182  pwinfi2  38184  ss2iundf  38268  neik0imk0p  38651  gneispace  38749  gneispace0nelrn  38755  ralbidar  38966  rexbidar  38967  uzubico2  40115  climuzlem  40293  xlimxrre  40375  bgoldbtbndlem2  42019  bgoldbtbndlem4  42021  mpt2exxg2  42441  iunord  42747
  Copyright terms: Public domain W3C validator