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

Theorem ralimi 2857
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 2855 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ral 2819
This theorem is referenced by:  ral2imiOLD  2859  r19.26  2989  r19.29  2997  rr19.3v  3245  rr19.28v  3246  reu3  3293  uniiunlem  3588  reupick2  3784  uniss2  4278  ss2iun  4341  iineq2  4343  iunss2  4370  disjss2  4420  disjeq2  4421  reusv2lem5  4652  reusv3i  4654  ssrel2  5092  issref  5379  dmmptg  5503  fununi  5653  fnmpt  5706  mpteqb  5963  chfnrn  5991  dffo5  6037  ffvresb  6051  fmptcof  6054  mpt22eqb  6394  ralrnmpt2  6400  tfis  6668  fun11uni  6738  fun11iun  6744  zfrep6  6752  fnmpt2  6852  mpt2exxg  6857  frxp  6893  smores  7023  riiner  7384  ixpn0  7501  boxriin  7511  unifi2  7809  wemaplem2  7971  xpwdomg  8010  rankonidlem  8245  acni3  8427  dfac5  8508  dfac12lem2  8523  kmlem6  8534  kmlem8  8536  kmlem13  8541  cfsmolem  8649  fin23lem40  8730  isf32lem2  8733  fin1a2s  8793  hsmexlem2  8806  hsmex3  8813  axcc4  8818  domtriomlem  8821  dcomex  8826  ac6num  8858  iundom  8916  unirnfdomd  8941  konigthlem  8942  iunctb  8948  gch3  9053  wununi  9083  wunpw  9084  wunpr  9086  eltsk2g  9128  tskpwss  9129  tskpw  9130  grupw  9172  gruurn  9175  intgru  9191  grothpw  9203  grothpwex  9204  grothomex  9206  axgroth3  9208  suplem1pr  9429  supexpr  9431  supsr  9488  fimaxre3  10491  xrsupexmnf  11495  xrinfmexpnf  11496  fsuppmapnn0fiublem  12063  fsuppmapnn0fiub  12064  fsuppmapnn0fiubex  12065  mptnn0fsuppd  12071  rexanre  13141  rexuz3  13143  cau3lem  13149  caubnd2  13152  caubnd  13153  rlim0  13293  rlim0lt  13294  climi2  13296  climi0  13297  climrlim2  13332  rlimres  13343  o1rlimmul  13403  caurcvg  13461  caurcvg2  13462  caucvg  13463  caucvgb  13464  sumeq2  13478  ndvdssub  13923  gcdcllem1  14007  vdwnnlem1  14371  imasaddfnlem  14782  catidex  14928  catlid  14937  catrid  14938  catcocl  14939  catpropd  14964  subcidcl  15070  funcid  15096  setcepi  15272  tsrss  15709  mgmidmo  15734  gsumval2  15832  issubg2  16018  gagrpid  16134  gaass  16137  dprdcntz  16841  dprddisj  16842  abveq0  17270  abvmul  17273  abvtri  17274  psgndiflemB  18419  phllmhm  18450  ipcj  18452  ipeq0  18456  mdetmul  18908  pmatcollpw2lem  19061  eltg2b  19243  iincld  19322  iuncld  19328  isclo2  19371  neips  19396  neipeltop  19412  lmcvg  19545  t1t0  19631  hauscmplem  19688  bwth  19692  1stcelcls  19744  ptuni2  19828  pttopon  19848  ptcld  19865  ptcnplem  19873  txtube  19892  txlm  19900  xkococnlem  19911  fbun  20092  isfil2  20108  ptcmplem4  20306  tmdcn2  20339  ustssel  20459  isucn2  20533  ucncn  20539  xmeteq0  20592  xmettri2  20594  metrest  20778  tngngp  20919  iscau4  21469  cmetcaulem  21478  caussi  21487  volfiniun  21708  iunmbl  21714  voliun  21715  mbfdm  21786  itg2seq  21900  itg2i1fseqle  21912  itg2i1fseq2  21914  iblcnlem  21946  limcresi  22040  limciun  22049  rolle  22142  ulmss  22542  rlimcnp  23039  midf  23835  colinearalg  23905  axpasch  23936  axeuclid  23958  axcontlem2  23960  axcontlem4  23962  axcontlem7  23965  axcontlem8  23966  nbgraf1olem1  24133  usgfiregdegfi  24603  1to3vfriendship  24700  frconngra  24713  frgraregorufr0  24745  usgreghash2spot  24762  isgrpo  24890  grpoidinv  24902  grpoideu  24903  grpoidval  24910  grpoidinv2  24912  opidon  25016  exidu1  25020  grpomndo  25040  rngoideu  25078  rngodi  25079  rngodir  25080  rngoass  25081  rngoueqz  25124  vcid  25136  vcdi  25137  vcdir  25138  vcass  25139  nvs  25257  nvz  25264  nvtri  25265  ajmoi  25466  adjmo  26443  cnlnssadj  26691  mdbr3  26908  mdbr4  26909  mdsl1i  26932  dmdbr6ati  27034  dmdbr7ati  27035  disjunsn  27142  fnmptf  27188  xrge0infss  27264  hasheuni  27747  sigaclcu2  27776  prsiga  27787  measvunilem  27839  cntmeas  27853  signsply0  28164  cvmsdisj  28371  cvmshmeo  28372  cvmliftlem15  28399  cvmlift2lem12  28415  untangtr  28577  prodeq2  28639  elpotr  28806  dfon2lem7  28814  dfon2lem8  28815  tfisg  28877  wfisg  28882  frinsg  28918  poseq  28926  heicant  29642  ovoliunnfl  29649  voliunnfl  29651  volsupnfl  29652  opnrebl2  29732  fnemeet2  29804  fnejoin1  29805  fnejoin2  29806  frinfm  29845  caushft  29873  sstotbnd3  29891  prdstotbnd  29909  heibor1lem  29924  bfplem2  29938  rngohomadd  29991  rngohommul  29992  idladdcl  30035  idllmulcl  30036  idlrmulcl  30037  ispridl2  30054  mpt2bi123f  30191  iineq12f  30193  mptbi12f  30195  lerabdioph  30358  ltrabdioph  30361  nerabdioph  30362  dvdsrabdioph  30363  rencldnfi  30375  dford3  30590  ralbidar  30948  rexbidar  30949  stoweidlem60  31376  mndsgrp  31945  mpt2exxg2  32011  bnj1498  33205  pmapglbx  34574  ltrnnid  34941  cdlemefrs32fva  35205
  Copyright terms: Public domain W3C validator