Theorem ralimi 3075

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 3072	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

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

This theorem depends on definitions:  df-bi 207  df-ral 3053

This theorem is referenced by:  rexbi  3094  ralrexbid  3095  r19.26  3098  r19.30  3105  2ralimi  3108  3ralimi  3109  4ralimi  3110  5ralimi  3111  6ralimi  3112  r19.21v  3163  rr19.3v  3610  rr19.28v  3611  reu3  3674  uniiunlem  4028  reupick2  4272  uniss2  4885  ss2iun  4953  iineq2  4955  dfiun2g  4973  iunss2  4993  disjss2  5056  disjeq2  5057  triin  5209  replem  5223  zfrep6  5224  reusv2lem5  5337  dmmptg  6198  frpoinsg  6299  fununi  6565  fnmptf  6626  fnmpt  6630  mpteqb  6959  chfnrn  6993  fvn0ssdmfun  7018  dffo5  7048  ffvresb  7070  fmptcof  7075  mpo2eqb  7490  ralrnmpo  7497  abnexg  7701  tfisg  7796  tfis  7797  fun11uni  7875  fiun  7887  f1iun  7888  zfrep6OLD  7899  mpoexxg  8019  el2mpocsbcl  8026  frxp  8067  xpord2indlem  8088  xpord3inddlem  8095  poseq  8099  smores  8283  naddcllem  8603  naddcom  8609  naddrid  8610  naddunif  8620  naddass  8623  riiner  8728  ixpn0  8869  boxriin  8879  unifi2  9246  wemaplem2  9453  frinsg  9664  rankonidlem  9741  acni3  9958  dfac5  10040  dfac12lem2  10056  kmlem6  10067  kmlem8  10069  kmlem13  10074  cfsmolem  10181  fin23lem40  10262  isf32lem2  10265  fin1a2s  10325  hsmexlem2  10338  hsmex3  10345  axcc4  10350  domtriomlem  10353  dcomex  10358  ac6num  10390  iundom  10453  unirnfdomd  10479  konigthlem  10480  iunctb  10486  gch3  10588  wununi  10618  wunpw  10619  wunpr  10621  eltsk2g  10663  tskpwss  10664  tskpw  10665  grupw  10707  gruurn  10710  intgru  10726  grothpw  10738  grothpwex  10739  grothomex  10741  axgroth3  10743  suplem1pr  10964  supexpr  10966  supsr  11024  fimaxre3  12089  xrsupexmnf  13221  xrinfmexpnf  13222  fsuppmapnn0fiublem  13914  fsuppmapnn0fiub  13915  fsuppmapnn0fiubex  13916  mptnn0fsuppd  13922  rexanre  15271  rexuz3  15273  cau3lem  15279  caubnd2  15282  caubnd  15283  rlim0  15432  rlim0lt  15433  climi2  15435  climi0  15436  climrlim2  15471  rlimres  15482  o1rlimmul  15543  caurcvg  15601  caurcvg2  15602  caucvg  15603  caucvgb  15604  sumeq2  15618  prodeq2  15836  ndvdssub  16337  gcdcllem1  16427  coprmproddvdslem  16590  vdwnnlem1  16924  imasaddfnlem  17450  catidex  17598  catlid  17607  catrid  17608  catcocl  17609  catpropd  17633  subcidcl  17769  funcid  17795  setcepi  18013  tsrss  18513  mgmidmo  18586  gsumval2  18612  isnmnd  18664  issubg2  19075  gagrpid  19227  gaass  19230  cygabl  19824  dprdcntz  19943  dprddisj  19944  abveq0  20753  abvmul  20756  abvtri  20757  psgndiflemB  21557  phllmhm  21589  ipcj  21591  ipeq0  21595  mdetmul  22566  pmatcollpw2lem  22720  eltg2b  22902  iincld  22982  iuncld  22988  isclo2  23031  neips  23056  neipeltop  23072  lmcvg  23205  t1t0  23291  hauscmplem  23349  bwth  23353  1stcelcls  23404  ptuni2  23519  pttopon  23539  ptcld  23556  ptcnplem  23564  txtube  23583  txlm  23591  xkococnlem  23602  fbun  23783  isfil2  23799  ptcmplem4  23998  ustssel  24149  isucn2  24221  ucncn  24227  metrest  24467  tngngp  24597  tngngp3  24599  ncvsi  25096  iscau4  25224  cmetcaulem  25233  caussi  25242  volfiniun  25492  iunmbl  25498  voliun  25499  mbfdm  25571  itg2seq  25687  itg2i1fseqle  25699  itg2i1fseq2  25701  iblcnlem  25734  limcresi  25830  limciun  25839  rolle  25935  ulmss  26346  rlimcnp  26915  madebdayim  27868  addsuniflem  27981  oldfib  28357  colinearalg  28967  axpasch  28998  axeuclid  29020  axcontlem2  29022  axcontlem4  29024  axcontlem7  29027  axcontlem8  29028  fusgrregdegfi  29627  0grrgr  29638  rusgr1vtxlem  29645  wlkvtxeledg  29681  wlkdlem3  29740  wlkdlem4  29741  lfgriswlk  29744  lfgrwlknloop  29745  eulercrct  30301  1to3vfriendship  30340  frgrregorufr0  30383  isgrpo  30557  grpoidinv  30568  grpoideu  30569  grpoidval  30573  grpoidinv2  30575  vcidOLD  30624  vcdi  30625  vcdir  30626  vcass  30627  nvs  30723  nvz  30729  nvtri  30730  mdbr3  32357  mdbr4  32358  mdsl1i  32381  dmdbr6ati  32483  dmdbr7ati  32484  disjunsn  32653  hasheuni  34235  sigaclcu2  34270  prsiga  34281  measvunilem  34362  cntmeas  34376  omssubadd  34450  signsply0  34701  bnj1498  35209  nummin  35242  axprALT2  35259  tz9.1regs  35284  onvf1odlem4  35294  lfuhgr2  35307  cvmsdisj  35458  cvmshmeo  35459  cvmliftlem15  35486  cvmlift2lem12  35502  untangtr  35902  elpotr  35967  dfon2lem7  35975  dfon2lem8  35976  opnrebl2  36509  fnemeet2  36555  fnejoin1  36556  fnejoin2  36557  weiunso  36654  weiunse  36656  weiunwe  36657  dfgcd3  37636  domalom  37716  ctbssinf  37718  nlpfvineqsn  37721  fvineqsnf1  37722  pibt1  37728  pibt2  37729  ptrecube  37932  poimirlem25  37957  poimirlem26  37958  poimirlem27  37959  poimirlem30  37962  poimirlem31  37963  poimirlem32  37964  heicant  37967  ovoliunnfl  37974  voliunnfl  37976  volsupnfl  37977  frinfm  38047  caushft  38073  sstotbnd3  38088  prdstotbnd  38106  heibor1lem  38121  bfplem2  38135  opidonOLD  38164  exidu1  38168  grpomndo  38187  rngoideu  38215  rngodi  38216  rngodir  38217  rngoass  38218  rngoueqz  38252  idladdcl  38331  idllmulcl  38332  idlrmulcl  38333  mpobi123f  38474  iineq12f  38476  mptbi12f  38478  dmqsblocks  39279  pmapglbx  40206  ltrnnid  40573  cdlemefrs32fva  40837  unitscyglem3  42628  fsuppind  43022  dffltz  43066  lerabdioph  43236  ltrabdioph  43239  nerabdioph  43240  dvdsrabdioph  43241  rencldnfi  43252  dford3  43459  pwelg  43990  pwinfi2  43992  ss2iundf  44089  neik0imk0p  44466  gneispace  44564  gneispace0nelrn  44570  ismnushort  44731  ralbidar  44874  rexbidar  44875  ssclaxsep  45412  uniclaxun  45416  uzubico2  46002  climuzlem  46175  xlimxrre  46263  natlocalincr  47308  2reuimp0  47548  bgoldbtbndlem2  48240  bgoldbtbndlem4  48242  mpoexxg2  48772  iuneqconst2  49256  iineqconst2  49257  iunord  50109