Theorem ralimi 3072

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

Syntax hints:   → wi 4   ∈ wcel 2098  ∀wral 3050

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

This theorem depends on definitions:  df-bi 206  df-ral 3051

This theorem is referenced by:  rexbi  3093  ralrexbid  3095  r19.35OLD  3098  r19.26  3100  r19.29OLD  3104  r19.30  3109  r19.30OLD  3110  2ralimi  3112  3ralimi  3113  4ralimi  3114  5ralimi  3115  6ralimi  3116  r19.21v  3169  rr19.3v  3652  rr19.28v  3653  reu3  3719  uniiunlem  4080  reupick2  4320  ralf0  4515  uniss2  4945  ss2iun  5015  iineq2  5017  dfiun2g  5034  iunss2  5053  disjss2  5117  disjeq2  5118  triin  5283  reusv2lem5  5402  dmmptg  6248  frpoinsg  6351  wfisgOLD  6362  fununi  6629  fnmptf  6692  fnmpt  6696  mpteqb  7023  chfnrn  7057  fvn0ssdmfun  7083  dffo5  7113  ffvresb  7134  fmptcof  7139  mpo2eqb  7553  ralrnmpo  7560  abnexg  7759  tfisg  7859  tfis  7860  fun11uni  7941  fiun  7947  f1iun  7948  zfrep6  7959  mpoexxg  8080  el2mpocsbcl  8090  frxp  8131  xpord2indlem  8152  xpord3inddlem  8159  poseq  8163  smores  8373  naddcllem  8697  naddcom  8703  naddrid  8704  naddunif  8714  naddass  8717  riiner  8809  ixpn0  8949  boxriin  8959  unifi2  9373  wemaplem2  9577  frinsg  9781  rankonidlem  9858  acni3  10077  dfac5  10158  dfac12lem2  10174  kmlem6  10185  kmlem8  10187  kmlem13  10192  cfsmolem  10300  fin23lem40  10381  isf32lem2  10384  fin1a2s  10444  hsmexlem2  10457  hsmex3  10464  axcc4  10469  domtriomlem  10472  dcomex  10477  ac6num  10509  iundom  10572  unirnfdomd  10597  konigthlem  10598  iunctb  10604  gch3  10706  wununi  10736  wunpw  10737  wunpr  10739  eltsk2g  10781  tskpwss  10782  tskpw  10783  grupw  10825  gruurn  10828  intgru  10844  grothpw  10856  grothpwex  10857  grothomex  10859  axgroth3  10861  suplem1pr  11082  supexpr  11084  supsr  11142  fimaxre3  12198  xrsupexmnf  13324  xrinfmexpnf  13325  fsuppmapnn0fiublem  13996  fsuppmapnn0fiub  13997  fsuppmapnn0fiubex  13998  mptnn0fsuppd  14004  rexanre  15334  rexuz3  15336  cau3lem  15342  caubnd2  15345  caubnd  15346  rlim0  15493  rlim0lt  15494  climi2  15496  climi0  15497  climrlim2  15532  rlimres  15543  o1rlimmul  15604  caurcvg  15664  caurcvg2  15665  caucvg  15666  caucvgb  15667  sumeq2  15681  prodeq2  15899  ndvdssub  16394  gcdcllem1  16482  coprmproddvdslem  16641  vdwnnlem1  16972  imasaddfnlem  17518  catidex  17662  catlid  17671  catrid  17672  catcocl  17673  catpropd  17697  subcidcl  17838  funcid  17864  setcepi  18085  tsrss  18589  mgmidmo  18628  gsumval2  18654  isnmnd  18706  issubg2  19109  gagrpid  19262  gaass  19265  cygabl  19863  dprdcntz  19982  dprddisj  19983  abveq0  20723  abvmul  20726  abvtri  20727  psgndiflemB  21554  phllmhm  21586  ipcj  21588  ipeq0  21592  mdetmul  22574  pmatcollpw2lem  22728  eltg2b  22911  iincld  22992  iuncld  22998  isclo2  23041  neips  23066  neipeltop  23082  lmcvg  23215  t1t0  23301  hauscmplem  23359  bwth  23363  1stcelcls  23414  ptuni2  23529  pttopon  23549  ptcld  23566  ptcnplem  23574  txtube  23593  txlm  23601  xkococnlem  23612  fbun  23793  isfil2  23809  ptcmplem4  24008  ustssel  24159  isucn2  24233  ucncn  24239  metrest  24482  tngngp  24620  tngngp3  24622  ncvsi  25128  iscau4  25256  cmetcaulem  25265  caussi  25274  volfiniun  25525  iunmbl  25531  voliun  25532  mbfdm  25604  itg2seq  25721  itg2i1fseqle  25733  itg2i1fseq2  25735  iblcnlem  25767  limcresi  25863  limciun  25872  rolle  25971  ulmss  26383  rlimcnp  26947  madebdayim  27865  addsuniflem  27969  colinearalg  28798  axpasch  28829  axeuclid  28851  axcontlem2  28853  axcontlem4  28855  axcontlem7  28858  axcontlem8  28859  fusgrregdegfi  29460  0grrgr  29471  rusgr1vtxlem  29478  wlkvtxeledg  29515  wlkdlem3  29575  wlkdlem4  29576  lfgriswlk  29579  lfgrwlknloop  29580  eulercrct  30129  1to3vfriendship  30168  frgrregorufr0  30211  isgrpo  30384  grpoidinv  30395  grpoideu  30396  grpoidval  30400  grpoidinv2  30402  vcidOLD  30451  vcdi  30452  vcdir  30453  vcass  30454  nvs  30550  nvz  30556  nvtri  30557  mdbr3  32184  mdbr4  32185  mdsl1i  32208  dmdbr6ati  32310  dmdbr7ati  32311  disjunsn  32468  hasheuni  33837  sigaclcu2  33872  prsiga  33883  measvunilem  33964  cntmeas  33978  omssubadd  34053  signsply0  34316  bnj1498  34825  nummin  34847  lfuhgr2  34861  cvmsdisj  35013  cvmshmeo  35014  cvmliftlem15  35041  cvmlift2lem12  35057  untangtr  35441  elpotr  35510  dfon2lem7  35518  dfon2lem8  35519  opnrebl2  35938  fnemeet2  35984  fnejoin1  35985  fnejoin2  35986  dfgcd3  36936  domalom  37016  ctbssinf  37018  nlpfvineqsn  37021  fvineqsnf1  37022  pibt1  37028  pibt2  37029  ptrecube  37226  poimirlem25  37251  poimirlem26  37252  poimirlem27  37253  poimirlem30  37256  poimirlem31  37257  poimirlem32  37258  heicant  37261  ovoliunnfl  37268  voliunnfl  37270  volsupnfl  37271  frinfm  37341  caushft  37367  sstotbnd3  37382  prdstotbnd  37400  heibor1lem  37415  bfplem2  37429  opidonOLD  37458  exidu1  37462  grpomndo  37481  rngoideu  37509  rngodi  37510  rngodir  37511  rngoass  37512  rngoueqz  37546  idladdcl  37625  idllmulcl  37626  idlrmulcl  37627  mpobi123f  37768  iineq12f  37770  mptbi12f  37772  pmapglbx  39374  ltrnnid  39741  cdlemefrs32fva  40005  fsuppind  41960  dffltz  42195  lerabdioph  42369  ltrabdioph  42372  nerabdioph  42373  dvdsrabdioph  42374  rencldnfi  42385  dford3  42593  pwelg  43134  pwinfi2  43136  ss2iundf  43233  neik0imk0p  43610  gneispace  43708  gneispace0nelrn  43714  ismnushort  43882  ralbidar  44026  rexbidar  44027  uzubico2  45095  climuzlem  45271  xlimxrre  45359  natlocalincr  46402  2reuimp0  46634  bgoldbtbndlem2  47285  bgoldbtbndlem4  47287  mpoexxg2  47589  iunord  48295