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

Theorem ralimi 2936
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 2934 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-ral 2901
This theorem is referenced by:  r19.26  3046  r19.29  3054  rr19.3v  3314  rr19.28v  3315  reu3  3363  uniiunlem  3653  reupick2  3872  uniss2  4406  ss2iun  4472  iineq2  4474  iunss2  4501  disjss2  4556  disjeq2  4557  reusv2lem5  4799  reusv3i  4801  ssrel2  5133  issref  5428  dmmptg  5549  wfisg  5632  fununi  5878  fnmptf  5929  fnmpt  5933  mpteqb  6207  chfnrn  6236  fvn0ssdmfun  6258  dffo5  6284  ffvresb  6301  fmptcof  6304  mpt22eqb  6667  ralrnmpt2  6673  tfis  6946  fun11uni  7013  fun11iun  7019  zfrep6  7027  fnmpt2  7127  mpt2exxg  7133  el2mpt2csbcl  7137  frxp  7174  smores  7336  riiner  7707  ixpn0  7826  boxriin  7836  unifi2  8139  wemaplem2  8335  xpwdomg  8373  rankonidlem  8574  acni3  8753  dfac5  8834  dfac12lem2  8849  kmlem6  8860  kmlem8  8862  kmlem13  8867  cfsmolem  8975  fin23lem40  9056  isf32lem2  9059  fin1a2s  9119  hsmexlem2  9132  hsmex3  9139  axcc4  9144  domtriomlem  9147  dcomex  9152  ac6num  9184  iundom  9243  unirnfdomd  9268  konigthlem  9269  iunctb  9275  gch3  9377  wununi  9407  wunpw  9408  wunpr  9410  eltsk2g  9452  tskpwss  9453  tskpw  9454  grupw  9496  gruurn  9499  intgru  9515  grothpw  9527  grothpwex  9528  grothomex  9530  axgroth3  9532  suplem1pr  9753  supexpr  9755  supsr  9812  fimaxre3  10849  xrsupexmnf  12007  xrinfmexpnf  12008  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  fsuppmapnn0fiubex  12654  mptnn0fsuppd  12660  rexanre  13934  rexuz3  13936  cau3lem  13942  caubnd2  13945  caubnd  13946  rlim0  14087  rlim0lt  14088  climi2  14090  climi0  14091  climrlim2  14126  rlimres  14137  o1rlimmul  14197  caurcvg  14255  caurcvg2  14256  caucvg  14257  caucvgb  14258  sumeq2  14272  prodeq2  14483  ndvdssub  14971  gcdcllem1  15059  coprmproddvdslem  15214  vdwnnlem1  15537  imasaddfnlem  16011  catidex  16158  catlid  16167  catrid  16168  catcocl  16169  catpropd  16192  subcidcl  16327  funcid  16353  setcepi  16561  tsrss  17046  mgmidmo  17082  gsumval2  17103  isnmnd  17121  dfgrp3e  17338  issubg2  17432  gagrpid  17550  gaass  17553  dprdcntz  18230  dprddisj  18231  abveq0  18649  abvmul  18652  abvtri  18653  psgndiflemB  19765  phllmhm  19796  ipcj  19798  ipeq0  19802  mdetmul  20248  pmatcollpw2lem  20401  eltg2b  20574  iincld  20653  iuncld  20659  isclo2  20702  neips  20727  neipeltop  20743  lmcvg  20876  t1t0  20962  hauscmplem  21019  bwth  21023  1stcelcls  21074  ptuni2  21189  pttopon  21209  ptcld  21226  ptcnplem  21234  txtube  21253  txlm  21261  xkococnlem  21272  fbun  21454  isfil2  21470  ptcmplem4  21669  tmdcn2  21703  ustssel  21819  isucn2  21893  ucncn  21899  xmeteq0  21953  xmettri2  21955  metrest  22139  tngngp  22268  tngngp3  22270  ncvsi  22759  iscau4  22885  cmetcaulem  22894  caussi  22903  volfiniun  23122  iunmbl  23128  voliun  23129  mbfdm  23201  itg2seq  23315  itg2i1fseqle  23327  itg2i1fseq2  23329  iblcnlem  23361  limcresi  23455  limciun  23464  rolle  23557  ulmss  23955  rlimcnp  24492  midf  25468  colinearalg  25590  axpasch  25621  axeuclid  25643  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  nbgraf1olem1  25970  usgfiregdegfi  26438  1to3vfriendship  26535  frconngra  26548  frgraregorufr0  26579  usgreghash2spot  26596  isgrpo  26735  grpoidinv  26746  grpoideu  26747  grpoidval  26751  grpoidinv2  26753  vcidOLD  26803  vcdi  26804  vcdir  26805  vcass  26806  nvs  26902  nvz  26908  nvtri  26909  ajmoi  27098  adjmo  28075  cnlnssadj  28323  mdbr3  28540  mdbr4  28541  mdsl1i  28564  dmdbr6ati  28666  dmdbr7ati  28667  disjunsn  28789  hasheuni  29474  sigaclcu2  29510  prsiga  29521  measvunilem  29602  cntmeas  29616  omssubadd  29689  signsply0  29954  bnj1498  30383  cvmsdisj  30506  cvmshmeo  30507  cvmliftlem15  30534  cvmlift2lem12  30550  untangtr  30845  elpotr  30930  dfon2lem7  30938  dfon2lem8  30939  tfisg  30960  frinsg  30986  poseq  30994  opnrebl2  31486  fnemeet2  31532  fnejoin1  31533  fnejoin2  31534  ptrecube  32579  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  heicant  32614  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  frinfm  32700  caushft  32727  sstotbnd3  32745  prdstotbnd  32763  heibor1lem  32778  bfplem2  32792  opidonOLD  32821  exidu1  32825  grpomndo  32844  rngoideu  32872  rngodi  32873  rngodir  32874  rngoass  32875  rngoueqz  32909  rngohomadd  32938  rngohommul  32939  idladdcl  32988  idllmulcl  32989  idlrmulcl  32990  ispridl2  33007  mpt2bi123f  33141  iineq12f  33143  mptbi12f  33145  pmapglbx  34073  ltrnnid  34440  cdlemefrs32fva  34706  lerabdioph  36387  ltrabdioph  36390  nerabdioph  36391  dvdsrabdioph  36392  rencldnfi  36403  dford3  36613  pwelg  36884  pwinfi2  36886  ss2iundf  36970  neik0imk0p  37354  ntrk2imkb  37355  gneispace  37452  gneispace0nelrn  37458  gneispaceel  37461  gneispacess  37463  ralbidar  37670  rexbidar  37671  stoweidlem60  38953  bgoldbtbndlem2  40222  bgoldbtbndlem4  40224  fusgrregdegfi  40769  0grrgr  40780  rusgr1vtxlem  40787  1wlkvtxeledg  40828  1wlkdlem3  40893  1wlkdlem4  40894  lfgriswlk  40897  lfgr1wlknloop  40898  eulercrct  41410  1to3vfriendship-av  41451  frgrconngr  41464  frgrregorufr0  41489  fusgreghash2wsp  41502  mpt2exxg2  41909  iunord  42220
  Copyright terms: Public domain W3C validator