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

Theorem ralimi 2773
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 2771 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   A.wral 2697
This theorem is referenced by:  ral2imi  2774  r19.26  2830  r19.29  2838  rr19.3v  3069  rr19.28v  3070  reu3  3116  uniiunlem  3423  reupick2  3619  uniss2  4038  ss2iun  4100  iineq2  4102  iunss2  4128  disjss2  4177  disjeq2  4178  reusv2lem5  4720  reusv3i  4722  tfis  4826  ssrel2  4958  issref  5239  dmmptg  5359  fununi  5509  fun11uni  5511  fnmpt  5563  fun11iun  5687  mpteqb  5811  chfnrn  5833  dffo5  5878  ffvresb  5892  fmptcof  5894  zfrep6  5960  mpt22eqb  6171  ralrnmpt2  6176  fnmpt2  6411  mpt2exxg  6414  frxp  6448  smores  6606  riiner  6969  ixpn0  7086  boxriin  7096  unifi2  7388  wemaplem2  7508  xpwdomg  7545  rankonidlem  7746  acni3  7920  dfac5  8001  dfac12lem2  8016  kmlem6  8027  kmlem8  8029  kmlem13  8034  cfsmolem  8142  fin23lem40  8223  isf32lem2  8226  fin1a2s  8286  hsmexlem2  8299  hsmex3  8306  axcc4  8311  domtriomlem  8314  dcomex  8319  ac6num  8351  iundom  8409  unirnfdomd  8434  konigthlem  8435  iunctb  8441  gch3  8547  wununi  8573  wunpw  8574  wunpr  8576  eltsk2g  8618  tskpwss  8619  tskpw  8620  grupw  8662  gruurn  8665  intgru  8681  grothpw  8693  grothpwex  8694  grothomex  8696  axgroth3  8698  suplem1pr  8921  supexpr  8923  supsr  8979  fimaxre3  9949  xrsupexmnf  10875  xrinfmexpnf  10876  rexanre  12142  rexuz3  12144  cau3lem  12150  caubnd2  12153  caubnd  12154  rlim0  12294  rlim0lt  12295  climi2  12297  climi0  12298  climrlim2  12333  rlimres  12344  o1rlimmul  12404  caurcvg  12462  caurcvg2  12463  caucvg  12464  caucvgb  12465  sumeq2  12480  ndvdssub  12919  gcdcllem1  13003  vdwnnlem1  13355  imasaddfnlem  13745  catidex  13891  catlid  13900  catrid  13901  catcocl  13902  catpropd  13927  subcidcl  14033  funcid  14059  setcepi  14235  tsrss  14647  laspwcl  14658  lanfwcl  14659  mgmidmo  14685  gsumval2  14775  issubg2  14951  gagrpid  15063  gaass  15066  dprdcntz  15558  dprddisj  15559  abveq0  15906  abvmul  15909  abvtri  15910  phllmhm  16855  ipcj  16857  ipeq0  16861  eltg2b  17016  iincld  17095  iuncld  17101  isclo2  17144  neips  17169  neipeltop  17185  lmcvg  17318  t1t0  17404  hauscmplem  17461  1stcelcls  17516  ptuni2  17600  pttopon  17620  ptcld  17637  ptcnplem  17645  txtube  17664  txlm  17672  xkococnlem  17683  fbun  17864  isfil2  17880  ptcmplem4  18078  tmdcn2  18111  ustssel  18227  isucn2  18301  ucncn  18307  xmeteq0  18360  xmettri2  18362  metrest  18546  tngngp  18687  iscau4  19224  cmetcaulem  19233  caussi  19242  volfiniun  19433  iunmbl  19439  voliun  19440  mbfdm  19512  itg2seq  19626  itg2i1fseqle  19638  itg2i1fseq2  19640  iblcnlem  19672  limcresi  19764  limciun  19773  rolle  19866  ulmss  20305  rlimcnp  20796  nbgraf1olem1  21443  isgrpo  21776  grpoidinv  21788  grpoideu  21789  grpoidval  21796  grpoidinv2  21798  opidon  21902  exidu1  21906  grpomndo  21926  rngoideu  21964  rngodi  21965  rngodir  21966  rngoass  21967  rngoueqz  22010  vcid  22022  vcdi  22023  vcdir  22024  vcass  22025  nvs  22143  nvz  22150  nvtri  22151  ajmoi  22352  adjmo  23327  cnlnssadj  23575  mdbr3  23792  mdbr4  23793  mdsl1i  23816  dmdbr6ati  23918  dmdbr7ati  23919  fnmptf  24066  hasheuni  24467  sigaclcu2  24495  prsiga  24506  measvunilem  24558  cntmeas  24572  cvmsdisj  24949  cvmshmeo  24950  cvmliftlem15  24977  cvmlift2lem12  24993  untangtr  25155  prodeq2  25232  elpotr  25400  dfon2lem7  25408  dfon2lem8  25409  tfisg  25471  wfisg  25476  frinsg  25512  poseq  25520  colinearalg  25841  axpasch  25872  axeuclid  25894  axcontlem2  25896  axcontlem4  25898  axcontlem7  25901  axcontlem8  25902  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  opnrebl2  26315  fnemeet2  26387  fnejoin1  26388  fnejoin2  26389  frinfm  26428  caushft  26458  sstotbnd3  26476  prdstotbnd  26494  heibor1lem  26509  bfplem2  26523  rngohomadd  26576  rngohommul  26577  idladdcl  26620  idllmulcl  26621  idlrmulcl  26622  ispridl2  26639  lerabdioph  26856  ltrabdioph  26859  nerabdioph  26860  dvdsrabdioph  26861  rencldnfi  26873  dford3  27090  ralbidar  27615  rexbidar  27616  stoweidlem60  27776  usgfiregdegfi  28314  1to3vfriendship  28335  frconngra  28348  frgraregorufr0  28378  usgreghash2spot  28395  bnj1498  29367  pmapglbx  30503  ltrnnid  30870  cdlemefrs32fva  31134
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ral 2702
  Copyright terms: Public domain W3C validator