Theorem ralimi 3080

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∀wral 3058

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

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

This theorem is referenced by:  rexbi  3101  ralrexbid  3103  r19.35OLD  3106  r19.26  3108  r19.29OLD  3112  r19.30  3117  r19.30OLD  3118  2ralimi  3120  3ralimi  3121  4ralimi  3122  5ralimi  3123  6ralimi  3124  r19.21v  3177  rr19.3v  3666  rr19.28v  3667  reu3  3735  uniiunlem  4096  reupick2  4336  ralf0  4519  uniss2  4945  ss2iun  5014  iineq2  5016  dfiun2g  5034  iunss2  5053  disjss2  5117  disjeq2  5118  triin  5281  reusv2lem5  5407  dmmptg  6263  frpoinsg  6365  wfisgOLD  6376  fununi  6642  fnmptf  6704  fnmpt  6708  mpteqb  7034  chfnrn  7068  fvn0ssdmfun  7093  dffo5  7123  ffvresb  7144  fmptcof  7149  mpo2eqb  7564  ralrnmpo  7571  abnexg  7774  tfisg  7874  tfis  7875  fun11uni  7955  fiun  7965  f1iun  7966  zfrep6  7977  mpoexxg  8098  el2mpocsbcl  8108  frxp  8149  xpord2indlem  8170  xpord3inddlem  8177  poseq  8181  smores  8390  naddcllem  8712  naddcom  8718  naddrid  8719  naddunif  8729  naddass  8732  riiner  8828  ixpn0  8968  boxriin  8978  unifi2  9382  wemaplem2  9584  frinsg  9788  rankonidlem  9865  acni3  10084  dfac5  10166  dfac12lem2  10182  kmlem6  10193  kmlem8  10195  kmlem13  10200  cfsmolem  10307  fin23lem40  10388  isf32lem2  10391  fin1a2s  10451  hsmexlem2  10464  hsmex3  10471  axcc4  10476  domtriomlem  10479  dcomex  10484  ac6num  10516  iundom  10579  unirnfdomd  10604  konigthlem  10605  iunctb  10611  gch3  10713  wununi  10743  wunpw  10744  wunpr  10746  eltsk2g  10788  tskpwss  10789  tskpw  10790  grupw  10832  gruurn  10835  intgru  10851  grothpw  10863  grothpwex  10864  grothomex  10866  axgroth3  10868  suplem1pr  11089  supexpr  11091  supsr  11149  fimaxre3  12211  xrsupexmnf  13343  xrinfmexpnf  13344  fsuppmapnn0fiublem  14027  fsuppmapnn0fiub  14028  fsuppmapnn0fiubex  14029  mptnn0fsuppd  14035  rexanre  15381  rexuz3  15383  cau3lem  15389  caubnd2  15392  caubnd  15393  rlim0  15540  rlim0lt  15541  climi2  15543  climi0  15544  climrlim2  15579  rlimres  15590  o1rlimmul  15651  caurcvg  15709  caurcvg2  15710  caucvg  15711  caucvgb  15712  sumeq2  15726  prodeq2  15944  ndvdssub  16442  gcdcllem1  16532  coprmproddvdslem  16695  vdwnnlem1  17028  imasaddfnlem  17574  catidex  17718  catlid  17727  catrid  17728  catcocl  17729  catpropd  17753  subcidcl  17894  funcid  17920  setcepi  18141  tsrss  18646  mgmidmo  18685  gsumval2  18711  isnmnd  18763  issubg2  19171  gagrpid  19324  gaass  19327  cygabl  19923  dprdcntz  20042  dprddisj  20043  abveq0  20835  abvmul  20838  abvtri  20839  psgndiflemB  21635  phllmhm  21667  ipcj  21669  ipeq0  21673  mdetmul  22644  pmatcollpw2lem  22798  eltg2b  22981  iincld  23062  iuncld  23068  isclo2  23111  neips  23136  neipeltop  23152  lmcvg  23285  t1t0  23371  hauscmplem  23429  bwth  23433  1stcelcls  23484  ptuni2  23599  pttopon  23619  ptcld  23636  ptcnplem  23644  txtube  23663  txlm  23671  xkococnlem  23682  fbun  23863  isfil2  23879  ptcmplem4  24078  ustssel  24229  isucn2  24303  ucncn  24309  metrest  24552  tngngp  24690  tngngp3  24692  ncvsi  25198  iscau4  25326  cmetcaulem  25335  caussi  25344  volfiniun  25595  iunmbl  25601  voliun  25602  mbfdm  25674  itg2seq  25791  itg2i1fseqle  25803  itg2i1fseq2  25805  iblcnlem  25838  limcresi  25934  limciun  25943  rolle  26042  ulmss  26454  rlimcnp  27022  madebdayim  27940  addsuniflem  28048  colinearalg  28939  axpasch  28970  axeuclid  28992  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  fusgrregdegfi  29601  0grrgr  29612  rusgr1vtxlem  29619  wlkvtxeledg  29656  wlkdlem3  29716  wlkdlem4  29717  lfgriswlk  29720  lfgrwlknloop  29721  eulercrct  30270  1to3vfriendship  30309  frgrregorufr0  30352  isgrpo  30525  grpoidinv  30536  grpoideu  30537  grpoidval  30541  grpoidinv2  30543  vcidOLD  30592  vcdi  30593  vcdir  30594  vcass  30595  nvs  30691  nvz  30697  nvtri  30698  mdbr3  32325  mdbr4  32326  mdsl1i  32349  dmdbr6ati  32451  dmdbr7ati  32452  disjunsn  32613  hasheuni  34065  sigaclcu2  34100  prsiga  34111  measvunilem  34192  cntmeas  34206  omssubadd  34281  signsply0  34544  bnj1498  35053  nummin  35083  lfuhgr2  35102  cvmsdisj  35254  cvmshmeo  35255  cvmliftlem15  35282  cvmlift2lem12  35298  untangtr  35693  elpotr  35762  dfon2lem7  35770  dfon2lem8  35771  opnrebl2  36303  fnemeet2  36349  fnejoin1  36350  fnejoin2  36351  weiunso  36448  weiunse  36450  weiunwe  36451  dfgcd3  37306  domalom  37386  ctbssinf  37388  nlpfvineqsn  37391  fvineqsnf1  37392  pibt1  37398  pibt2  37399  ptrecube  37606  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  heicant  37641  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  frinfm  37721  caushft  37747  sstotbnd3  37762  prdstotbnd  37780  heibor1lem  37795  bfplem2  37809  opidonOLD  37838  exidu1  37842  grpomndo  37861  rngoideu  37889  rngodi  37890  rngodir  37891  rngoass  37892  rngoueqz  37926  idladdcl  38005  idllmulcl  38006  idlrmulcl  38007  mpobi123f  38148  iineq12f  38150  mptbi12f  38152  pmapglbx  39751  ltrnnid  40118  cdlemefrs32fva  40382  unitscyglem3  42178  fsuppind  42576  dffltz  42620  lerabdioph  42792  ltrabdioph  42795  nerabdioph  42796  dvdsrabdioph  42797  rencldnfi  42808  dford3  43016  pwelg  43549  pwinfi2  43551  ss2iundf  43648  neik0imk0p  44025  gneispace  44123  gneispace0nelrn  44129  ismnushort  44296  ralbidar  44440  rexbidar  44441  ssclaxsep  44946  uzubico2  45522  climuzlem  45698  xlimxrre  45786  natlocalincr  46829  2reuimp0  47063  bgoldbtbndlem2  47730  bgoldbtbndlem4  47732  mpoexxg2  48182  iunord  48906