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

Theorem ralimi 2786
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 2784 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   A.wral 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-ral 2715
This theorem is referenced by:  ral2imi  2787  r19.26  2844  r19.29  2852  rr19.3v  3096  rr19.28v  3097  reu3  3144  uniiunlem  3435  reupick2  3631  uniss2  4119  ss2iun  4181  iineq2  4183  iunss2  4210  disjss2  4260  disjeq2  4261  reusv2lem5  4492  reusv3i  4494  ssrel2  4925  issref  5206  dmmptg  5330  fununi  5479  fnmpt  5532  mpteqb  5783  chfnrn  5809  dffo5  5855  ffvresb  5869  fmptcof  5872  mpt22eqb  6194  ralrnmpt2  6200  tfis  6460  fun11uni  6526  fun11iun  6532  zfrep6  6540  fnmpt2  6637  mpt2exxg  6642  frxp  6677  smores  6805  riiner  7165  ixpn0  7287  boxriin  7297  unifi2  7593  wemaplem2  7753  xpwdomg  7792  rankonidlem  8027  acni3  8209  dfac5  8290  dfac12lem2  8305  kmlem6  8316  kmlem8  8318  kmlem13  8323  cfsmolem  8431  fin23lem40  8512  isf32lem2  8515  fin1a2s  8575  hsmexlem2  8588  hsmex3  8595  axcc4  8600  domtriomlem  8603  dcomex  8608  ac6num  8640  iundom  8698  unirnfdomd  8723  konigthlem  8724  iunctb  8730  gch3  8835  wununi  8865  wunpw  8866  wunpr  8868  eltsk2g  8910  tskpwss  8911  tskpw  8912  grupw  8954  gruurn  8957  intgru  8973  grothpw  8985  grothpwex  8986  grothomex  8988  axgroth3  8990  suplem1pr  9213  supexpr  9215  supsr  9271  fimaxre3  10271  xrsupexmnf  11259  xrinfmexpnf  11260  rexanre  12826  rexuz3  12828  cau3lem  12834  caubnd2  12837  caubnd  12838  rlim0  12978  rlim0lt  12979  climi2  12981  climi0  12982  climrlim2  13017  rlimres  13028  o1rlimmul  13088  caurcvg  13146  caurcvg2  13147  caucvg  13148  caucvgb  13149  sumeq2  13163  ndvdssub  13603  gcdcllem1  13687  vdwnnlem1  14048  imasaddfnlem  14458  catidex  14604  catlid  14613  catrid  14614  catcocl  14615  catpropd  14640  subcidcl  14746  funcid  14772  setcepi  14948  tsrss  15385  mgmidmo  15410  gsumval2  15504  issubg2  15687  gagrpid  15803  gaass  15806  dprdcntz  16480  dprddisj  16481  abveq0  16889  abvmul  16892  abvtri  16893  psgndiflemB  18005  phllmhm  18036  ipcj  18038  ipeq0  18042  mdetmul  18404  eltg2b  18539  iincld  18618  iuncld  18624  isclo2  18667  neips  18692  neipeltop  18708  lmcvg  18841  t1t0  18927  hauscmplem  18984  bwth  18988  1stcelcls  19040  ptuni2  19124  pttopon  19144  ptcld  19161  ptcnplem  19169  txtube  19188  txlm  19196  xkococnlem  19207  fbun  19388  isfil2  19404  ptcmplem4  19602  tmdcn2  19635  ustssel  19755  isucn2  19829  ucncn  19835  xmeteq0  19888  xmettri2  19890  metrest  20074  tngngp  20215  iscau4  20765  cmetcaulem  20774  caussi  20783  volfiniun  21003  iunmbl  21009  voliun  21010  mbfdm  21081  itg2seq  21195  itg2i1fseqle  21207  itg2i1fseq2  21209  iblcnlem  21241  limcresi  21335  limciun  21344  rolle  21437  ulmss  21837  rlimcnp  22334  colinearalg  23107  axpasch  23138  axeuclid  23160  axcontlem2  23162  axcontlem4  23164  axcontlem7  23167  axcontlem8  23168  nbgraf1olem1  23301  isgrpo  23634  grpoidinv  23646  grpoideu  23647  grpoidval  23654  grpoidinv2  23656  opidon  23760  exidu1  23764  grpomndo  23784  rngoideu  23822  rngodi  23823  rngodir  23824  rngoass  23825  rngoueqz  23868  vcid  23880  vcdi  23881  vcdir  23882  vcass  23883  nvs  24001  nvz  24008  nvtri  24009  ajmoi  24210  adjmo  25187  cnlnssadj  25435  mdbr3  25652  mdbr4  25653  mdsl1i  25676  dmdbr6ati  25778  dmdbr7ati  25779  disjunsn  25887  fnmptf  25928  xrge0infss  26004  hasheuni  26486  sigaclcu2  26515  prsiga  26526  measvunilem  26578  cntmeas  26592  signsply0  26904  cvmsdisj  27111  cvmshmeo  27112  cvmliftlem15  27139  cvmlift2lem12  27155  untangtr  27316  prodeq2  27378  elpotr  27545  dfon2lem7  27553  dfon2lem8  27554  tfisg  27616  wfisg  27621  frinsg  27657  poseq  27665  heicant  28379  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  opnrebl2  28469  fnemeet2  28541  fnejoin1  28542  fnejoin2  28543  frinfm  28582  caushft  28610  sstotbnd3  28628  prdstotbnd  28646  heibor1lem  28661  bfplem2  28675  rngohomadd  28728  rngohommul  28729  idladdcl  28772  idllmulcl  28773  idlrmulcl  28774  ispridl2  28791  mpt2bi123f  28928  iineq12f  28930  mptbi12f  28932  lerabdioph  29096  ltrabdioph  29099  nerabdioph  29100  dvdsrabdioph  29101  rencldnfi  29113  dford3  29330  ralbidar  29654  rexbidar  29655  stoweidlem60  29808  usgfiregdegfi  30481  1to3vfriendship  30553  frconngra  30566  frgraregorufr0  30598  usgreghash2spot  30615  mpt2exxg2  30680  fsuppmapnn0fiublem  30747  fsuppmapnn0fiub  30748  fsuppmapnn0fiubex  30749  scmatid  30805  pmatcollpw2lem  30820  bnj1498  31939  pmapglbx  33253  ltrnnid  33620  cdlemefrs32fva  33884
  Copyright terms: Public domain W3C validator