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

Theorem ralimi 2796
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ralimi  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3  |-  ( ph  ->  ps )
21a1i 11 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2794 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   A.wral 2753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652
This theorem depends on definitions:  df-bi 185  df-ral 2758
This theorem is referenced by:  ral2imiOLD  2798  r19.26  2933  r19.29  2941  rr19.3v  3190  rr19.28v  3191  reu3  3238  uniiunlem  3526  reupick2  3735  uniss2  4222  ss2iun  4286  iineq2  4288  iunss2  4315  disjss2  4368  disjeq2  4369  reusv2lem5  4598  reusv3i  4600  ssrel2  4913  issref  5200  dmmptg  5319  wfisg  5401  fununi  5634  fnmptf  5685  fnmpt  5689  mpteqb  5947  chfnrn  5975  fvn0ssdmfun  5999  dffo5  6025  ffvresb  6040  fmptcof  6043  mpt22eqb  6391  ralrnmpt2  6397  tfis  6671  fun11uni  6737  fun11iun  6743  zfrep6  6751  fnmpt2  6851  mpt2exxg  6857  frxp  6893  smores  7055  riiner  7420  ixpn0  7538  boxriin  7548  unifi2  7843  wemaplem2  8005  xpwdomg  8044  rankonidlem  8277  acni3  8459  dfac5  8540  dfac12lem2  8555  kmlem6  8566  kmlem8  8568  kmlem13  8573  cfsmolem  8681  fin23lem40  8762  isf32lem2  8765  fin1a2s  8825  hsmexlem2  8838  hsmex3  8845  axcc4  8850  domtriomlem  8853  dcomex  8858  ac6num  8890  iundom  8948  unirnfdomd  8973  konigthlem  8974  iunctb  8980  gch3  9083  wununi  9113  wunpw  9114  wunpr  9116  eltsk2g  9158  tskpwss  9159  tskpw  9160  grupw  9202  gruurn  9205  intgru  9221  grothpw  9233  grothpwex  9234  grothomex  9236  axgroth3  9238  suplem1pr  9459  supexpr  9461  supsr  9518  fimaxre3  10531  xrsupexmnf  11548  xrinfmexpnf  11549  fsuppmapnn0fiublem  12138  fsuppmapnn0fiub  12139  fsuppmapnn0fiubex  12140  mptnn0fsuppd  12146  rexanre  13326  rexuz3  13328  cau3lem  13334  caubnd2  13337  caubnd  13338  rlim0  13478  rlim0lt  13479  climi2  13481  climi0  13482  climrlim2  13517  rlimres  13528  o1rlimmul  13588  caurcvg  13646  caurcvg2  13647  caucvg  13648  caucvgb  13649  sumeq2  13663  prodeq2  13871  ndvdssub  14272  gcdcllem1  14356  vdwnnlem1  14720  imasaddfnlem  15140  catidex  15286  catlid  15295  catrid  15296  catcocl  15297  catpropd  15320  subcidcl  15455  funcid  15481  setcepi  15689  tsrss  16175  mgmidmo  16208  gsumval2  16229  isnmnd  16246  issubg2  16538  gagrpid  16654  gaass  16657  dprdcntz  17359  dprddisj  17360  abveq0  17793  abvmul  17796  abvtri  17797  psgndiflemB  18932  phllmhm  18963  ipcj  18965  ipeq0  18969  mdetmul  19415  pmatcollpw2lem  19568  eltg2b  19750  iincld  19830  iuncld  19836  isclo2  19880  neips  19905  neipeltop  19921  lmcvg  20054  t1t0  20140  hauscmplem  20197  bwth  20201  1stcelcls  20252  ptuni2  20367  pttopon  20387  ptcld  20404  ptcnplem  20412  txtube  20431  txlm  20439  xkococnlem  20450  fbun  20631  isfil2  20647  ptcmplem4  20845  tmdcn2  20878  ustssel  20998  isucn2  21072  ucncn  21078  xmeteq0  21131  xmettri2  21133  metrest  21317  tngngp  21458  iscau4  22008  cmetcaulem  22017  caussi  22026  volfiniun  22247  iunmbl  22253  voliun  22254  mbfdm  22325  itg2seq  22439  itg2i1fseqle  22451  itg2i1fseq2  22453  iblcnlem  22485  limcresi  22579  limciun  22588  rolle  22681  ulmss  23082  rlimcnp  23619  midf  24525  colinearalg  24617  axpasch  24648  axeuclid  24670  axcontlem2  24672  axcontlem4  24674  axcontlem7  24677  axcontlem8  24678  nbgraf1olem1  24845  usgfiregdegfi  25315  1to3vfriendship  25412  frconngra  25425  frgraregorufr0  25456  usgreghash2spot  25473  isgrpo  25598  grpoidinv  25610  grpoideu  25611  grpoidval  25618  grpoidinv2  25620  opidonOLD  25724  exidu1  25728  grpomndo  25748  rngoideu  25786  rngodi  25787  rngodir  25788  rngoass  25789  rngoueqz  25832  vcid  25844  vcdi  25845  vcdir  25846  vcass  25847  nvs  25965  nvz  25972  nvtri  25973  ajmoi  26174  adjmo  27150  cnlnssadj  27398  mdbr3  27615  mdbr4  27616  mdsl1i  27639  dmdbr6ati  27741  dmdbr7ati  27742  disjunsn  27872  xrge0infss  28008  hasheuni  28518  sigaclcu2  28554  prsiga  28565  measvunilem  28646  cntmeas  28660  omssubadd  28734  signsply0  29000  bnj1498  29431  cvmsdisj  29554  cvmshmeo  29555  cvmliftlem15  29582  cvmlift2lem12  29598  untangtr  29902  elpotr  29987  dfon2lem7  29995  dfon2lem8  29996  tfisg  30017  frinsg  30043  poseq  30051  opnrebl2  30536  fnemeet2  30582  fnejoin1  30583  fnejoin2  30584  heicant  31401  ovoliunnfl  31408  voliunnfl  31410  volsupnfl  31411  frinfm  31488  caushft  31516  sstotbnd3  31534  prdstotbnd  31552  heibor1lem  31567  bfplem2  31581  rngohomadd  31634  rngohommul  31635  idladdcl  31678  idllmulcl  31679  idlrmulcl  31680  ispridl2  31697  mpt2bi123f  31833  iineq12f  31835  mptbi12f  31837  pmapglbx  32766  ltrnnid  33133  cdlemefrs32fva  33399  lerabdioph  35080  ltrabdioph  35083  nerabdioph  35084  dvdsrabdioph  35085  rencldnfi  35096  dford3  35312  pwelg  35591  pwinfi2  35593  ss2iundf  35618  ralbidar  36182  rexbidar  36183  stoweidlem60  37191  bgoldbtbndlem2  37835  bgoldbtbndlem4  37837  mpt2exxg2  38419
  Copyright terms: Public domain W3C validator