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

Theorem ralimi 2781
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 2779 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605
This theorem depends on definitions:  df-bi 185  df-ral 2710
This theorem is referenced by:  ral2imi  2782  r19.26  2839  r19.29  2847  rr19.3v  3090  rr19.28v  3091  reu3  3138  uniiunlem  3428  reupick2  3624  uniss2  4112  ss2iun  4174  iineq2  4176  iunss2  4203  disjss2  4253  disjeq2  4254  reusv2lem5  4485  reusv3i  4487  ssrel2  4917  issref  5199  dmmptg  5323  fununi  5472  fnmpt  5525  mpteqb  5776  chfnrn  5802  dffo5  5848  ffvresb  5861  fmptcof  5864  mpt22eqb  6188  ralrnmpt2  6194  tfis  6454  fun11uni  6520  fun11iun  6526  zfrep6  6534  fnmpt2  6631  mpt2exxg  6636  frxp  6671  smores  6799  riiner  7161  ixpn0  7283  boxriin  7293  unifi2  7589  wemaplem2  7749  xpwdomg  7788  rankonidlem  8023  acni3  8205  dfac5  8286  dfac12lem2  8301  kmlem6  8312  kmlem8  8314  kmlem13  8319  cfsmolem  8427  fin23lem40  8508  isf32lem2  8511  fin1a2s  8571  hsmexlem2  8584  hsmex3  8591  axcc4  8596  domtriomlem  8599  dcomex  8604  ac6num  8636  iundom  8694  unirnfdomd  8719  konigthlem  8720  iunctb  8726  gch3  8830  wununi  8860  wunpw  8861  wunpr  8863  eltsk2g  8905  tskpwss  8906  tskpw  8907  grupw  8949  gruurn  8952  intgru  8968  grothpw  8980  grothpwex  8981  grothomex  8983  axgroth3  8985  suplem1pr  9208  supexpr  9210  supsr  9266  fimaxre3  10266  xrsupexmnf  11254  xrinfmexpnf  11255  rexanre  12817  rexuz3  12819  cau3lem  12825  caubnd2  12828  caubnd  12829  rlim0  12969  rlim0lt  12970  climi2  12972  climi0  12973  climrlim2  13008  rlimres  13019  o1rlimmul  13079  caurcvg  13137  caurcvg2  13138  caucvg  13139  caucvgb  13140  sumeq2  13154  ndvdssub  13593  gcdcllem1  13677  vdwnnlem1  14038  imasaddfnlem  14448  catidex  14594  catlid  14603  catrid  14604  catcocl  14605  catpropd  14630  subcidcl  14736  funcid  14762  setcepi  14938  tsrss  15375  mgmidmo  15400  gsumval2  15492  issubg2  15675  gagrpid  15791  gaass  15794  dprdcntz  16465  dprddisj  16466  abveq0  16834  abvmul  16837  abvtri  16838  psgndiflemB  17871  phllmhm  17902  ipcj  17904  ipeq0  17908  mdetmul  18270  eltg2b  18405  iincld  18484  iuncld  18490  isclo2  18533  neips  18558  neipeltop  18574  lmcvg  18707  t1t0  18793  hauscmplem  18850  bwth  18854  1stcelcls  18906  ptuni2  18990  pttopon  19010  ptcld  19027  ptcnplem  19035  txtube  19054  txlm  19062  xkococnlem  19073  fbun  19254  isfil2  19270  ptcmplem4  19468  tmdcn2  19501  ustssel  19621  isucn2  19695  ucncn  19701  xmeteq0  19754  xmettri2  19756  metrest  19940  tngngp  20081  iscau4  20631  cmetcaulem  20640  caussi  20649  volfiniun  20869  iunmbl  20875  voliun  20876  mbfdm  20947  itg2seq  21061  itg2i1fseqle  21073  itg2i1fseq2  21075  iblcnlem  21107  limcresi  21201  limciun  21210  rolle  21303  ulmss  21746  rlimcnp  22243  colinearalg  22978  axpasch  23009  axeuclid  23031  axcontlem2  23033  axcontlem4  23035  axcontlem7  23038  axcontlem8  23039  nbgraf1olem1  23172  isgrpo  23505  grpoidinv  23517  grpoideu  23518  grpoidval  23525  grpoidinv2  23527  opidon  23631  exidu1  23635  grpomndo  23655  rngoideu  23693  rngodi  23694  rngodir  23695  rngoass  23696  rngoueqz  23739  vcid  23751  vcdi  23752  vcdir  23753  vcass  23754  nvs  23872  nvz  23879  nvtri  23880  ajmoi  24081  adjmo  25058  cnlnssadj  25306  mdbr3  25523  mdbr4  25524  mdsl1i  25547  dmdbr6ati  25649  dmdbr7ati  25650  disjunsn  25759  fnmptf  25800  hasheuni  26387  sigaclcu2  26416  prsiga  26427  measvunilem  26479  cntmeas  26493  signsply0  26799  cvmsdisj  27006  cvmshmeo  27007  cvmliftlem15  27034  cvmlift2lem12  27050  untangtr  27211  prodeq2  27273  elpotr  27440  dfon2lem7  27448  dfon2lem8  27449  tfisg  27511  wfisg  27516  frinsg  27552  poseq  27560  heicant  28267  ovoliunnfl  28274  voliunnfl  28276  volsupnfl  28277  opnrebl2  28357  fnemeet2  28429  fnejoin1  28430  fnejoin2  28431  frinfm  28470  caushft  28498  sstotbnd3  28516  prdstotbnd  28534  heibor1lem  28549  bfplem2  28563  rngohomadd  28616  rngohommul  28617  idladdcl  28660  idllmulcl  28661  idlrmulcl  28662  ispridl2  28679  mpt2bi123f  28816  iineq12f  28818  mptbi12f  28820  lerabdioph  28985  ltrabdioph  28988  nerabdioph  28989  dvdsrabdioph  28990  rencldnfi  29002  dford3  29219  ralbidar  29543  rexbidar  29544  stoweidlem60  29698  usgfiregdegfi  30371  1to3vfriendship  30443  frconngra  30456  frgraregorufr0  30488  usgreghash2spot  30505  mpt2exxg2  30569  bnj1498  31751  pmapglbx  32983  ltrnnid  33350  cdlemefrs32fva  33614
  Copyright terms: Public domain W3C validator