Theorem ralimi 3098

Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ralimi	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	ralimia 3095	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828

This theorem depends on definitions:  df-bi 209  df-ral 3076

This theorem is referenced by:  rexbi  3117  ralrexbid  3118  r19.26  3121  r19.30  3128  2ralimi  3131  3ralimi  3132  4ralimi  3133  5ralimi  3134  6ralimi  3135  r19.21v  3186  rr19.3v  3625  rr19.28v  3626  reu3  3688  uniiunlem  4038  reupick2  4281  uniss2  4897  ss2iun  4965  iineq2  4967  dfiun2g  4984  iunss2  5004  disjss2  5067  disjeq2  5068  triin  5221  replem  5235  zfrep6  5236  reusv2lem5  5356  dmmptg  6224  frpoinsg  6325  fununi  6591  fnmptf  6652  fnmpt  6656  mpteqb  6990  chfnrn  7025  fvn0ssdmfun  7050  dffo5  7080  ffvresb  7102  fmptcof  7107  mpo2eqb  7523  ralrnmpo  7530  abnexg  7734  tfisg  7829  tfis  7830  fun11uni  7909  fiun  7919  f1iun  7920  zfrep6OLD  7931  mpoexxg  8051  el2mpocsbcl  8058  frxp  8100  xpord2indlem  8121  xpord3inddlem  8128  poseq  8132  smores  8317  naddcllem  8640  naddcom  8647  naddrid  8648  naddunif  8658  naddass  8661  riiner  8766  ixpn0  8906  boxriin  8916  unifi2  9282  wemaplem2  9489  frinsg  9703  rankonidlem  9780  acni3  9997  dfac5  10079  dfac12lem2  10095  kmlem6  10106  kmlem8  10108  kmlem13  10113  cfsmolem  10221  fin23lem40  10302  isf32lem2  10305  fin1a2s  10365  hsmexlem2  10378  hsmex3  10385  axcc4  10390  domtriomlem  10393  dcomex  10398  ac6num  10430  iundom  10493  unirnfdomd  10519  konigthlem  10520  iunctb  10526  gch3  10628  wununi  10658  wunpw  10659  wunpr  10661  eltsk2g  10703  tskpwss  10704  tskpw  10705  grupw  10747  gruurn  10750  intgru  10766  grothpw  10778  grothpwex  10779  grothomex  10781  axgroth3  10783  suplem1pr  11004  supexpr  11006  supsr  11064  fimaxre3  12132  xrsupexmnf  13302  xrinfmexpnf  13303  fsuppmapnn0fiublem  13997  fsuppmapnn0fiub  13998  fsuppmapnn0fiubex  13999  mptnn0fsuppd  14005  rexanre  15365  rexuz3  15367  cau3lem  15373  caubnd2  15376  caubnd  15377  rlim0  15526  rlim0lt  15527  climi2  15529  climi0  15530  climrlim2  15565  rlimres  15576  o1rlimmul  15637  caurcvg  15695  caurcvg2  15696  caucvg  15697  caucvgb  15698  sumeq2  15712  prodeq2  15933  ndvdssub  16434  gcdcllem1  16524  coprmproddvdslem  16687  vdwnnlem1  17022  imasaddfnlem  17549  catidex  17697  catlid  17706  catrid  17707  catcocl  17708  catpropd  17732  subcidcl  17868  funcid  17894  setcepi  18112  tsrss  18612  mgmidmo  18685  gsumval2  18711  isnmnd  18763  issubg2  19174  gagrpid  19325  gaass  19328  cygabl  19922  dprdcntz  20041  dprddisj  20042  abveq0  20855  abvmul  20858  abvtri  20859  psgndiflemB  21640  phllmhm  21672  ipcj  21674  ipeq0  21678  mdetmul  22671  pmatcollpw2lem  22825  eltg2b  23007  iincld  23087  iuncld  23093  isclo2  23136  neips  23161  neipeltop  23177  lmcvg  23310  t1t0  23396  hauscmplem  23454  bwth  23458  1stcelcls  23509  ptuni2  23624  pttopon  23644  ptcld  23661  ptcnplem  23669  txtube  23688  txlm  23696  xkococnlem  23707  fbun  23888  isfil2  23904  ptcmplem4  24103  ustssel  24254  isucn2  24326  ucncn  24332  metrest  24572  tngngp  24702  tngngp3  24704  ncvsi  25201  iscau4  25329  cmetcaulem  25338  caussi  25347  volfiniun  25597  iunmbl  25603  voliun  25604  mbfdm  25676  itg2seq  25792  itg2i1fseqle  25804  itg2i1fseq2  25806  iblcnlem  25839  limcresi  25935  limciun  25944  rolle  26040  ulmss  26448  rlimcnp  27018  madebdayim  27969  addsuniflem  28082  oldfib  28458  colinearalg  29068  axpasch  29099  axeuclid  29121  axcontlem2  29123  axcontlem4  29125  axcontlem7  29128  axcontlem8  29129  fusgrregdegfi  29727  0grrgr  29738  rusgr1vtxlem  29745  wlkvtxeledg  29781  wlkdlem3  29840  wlkdlem4  29841  lfgriswlk  29844  lfgrwlknloop  29845  eulercrct  30401  1to3vfriendship  30440  frgrregorufr0  30483  isgrpo  30657  grpoidinv  30668  grpoideu  30669  grpoidval  30673  grpoidinv2  30675  vcidOLD  30724  vcdi  30725  vcdir  30726  vcass  30727  nvs  30823  nvz  30829  nvtri  30830  mdbr3  32457  mdbr4  32458  mdsl1i  32481  dmdbr6ati  32583  dmdbr7ati  32584  disjunsn  32754  hasheuni  34343  sigaclcu2  34378  prsiga  34389  measvunilem  34470  cntmeas  34484  omssubadd  34558  signsply0  34806  bnj1498  35317  nummin  35350  axprALT2  35366  tz9.1regs  35391  onvf1odlem4  35410  lfuhgr2  35430  cvmsdisj  35581  cvmshmeo  35582  cvmliftlem15  35609  cvmlift2lem12  35625  untangtr  36025  elpotr  36090  dfon2lem7  36098  dfon2lem8  36099  nmulprop  36501  opnrebl2  36642  fnemeet2  36688  fnejoin1  36689  fnejoin2  36690  weiunso  36787  weiunse  36789  weiunwe  36790  dfgcd3  37777  domalom  37859  ctbssinf  37861  nlpfvineqsn  37864  fvineqsnf1  37865  pibt1  37871  pibt2  37872  ptrecube  38080  poimirlem25  38105  poimirlem26  38106  poimirlem27  38107  poimirlem30  38110  poimirlem31  38111  poimirlem32  38112  heicant  38115  ovoliunnfl  38122  voliunnfl  38124  volsupnfl  38125  frinfm  38195  caushft  38221  sstotbnd3  38236  prdstotbnd  38254  heibor1lem  38269  bfplem2  38283  opidonOLD  38312  exidu1  38316  grpomndo  38335  rngoideu  38363  rngodi  38364  rngodir  38365  rngoass  38366  rngoueqz  38400  idladdcl  38479  idllmulcl  38480  idlrmulcl  38481  mpobi123f  38622  iineq12f  38624  mptbi12f  38626  dmqsblocks  39427  pmapglbx  40354  ltrnnid  40721  cdlemefrs32fva  40985  unitscyglem3  42775  fsuppind  43133  dffltz  43177  lerabdioph  43343  ltrabdioph  43346  nerabdioph  43347  dvdsrabdioph  43348  rencldnfi  43359  dford3  43566  pwelg  44097  pwinfi2  44099  ss2iundf  44196  neik0imk0p  44573  gneispace  44671  gneispace0nelrn  44677  ismnushort  44838  ralbidar  44981  rexbidar  44982  ssclaxsep  45519  uniclaxun  45523  uzubico2  46105  climuzlem  46278  xlimxrre  46366  natlocalincr  47413  2reuimp0  47669  bgoldbtbndlem2  48389  bgoldbtbndlem4  48391  mpoexxg2  48921  iuneqconst2  49405  iineqconst2  49406  iunord  50258