Theorem ralimi 3099

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  rexbi  3118  ralrexbid  3119  r19.26  3122  r19.30  3129  2ralimi  3132  3ralimi  3133  4ralimi  3134  5ralimi  3135  6ralimi  3136  r19.21v  3187  rr19.3v  3621  rr19.28v  3622  reu3  3685  uniiunlem  4035  reupick2  4277  uniss2  4902  ss2iun  4970  iineq2  4972  dfiun2g  4988  iunss2  5008  disjss2  5073  disjeq2  5074  triin  5229  replem  5243  zfrep6  5244  reusv2lem5  5367  dmmptg  6238  frpoinsg  6341  fununi  6608  fnmptf  6668  fnmpt  6672  mpteqb  7006  chfnrn  7041  fvn0ssdmfun  7067  dffo5  7097  ffvresb  7119  fmptcof  7124  mpo2eqb  7545  ralrnmpo  7552  abnexg  7755  tfisg  7850  tfis  7851  fun11uni  7930  fiun  7940  f1iun  7941  zfrep6OLD  7952  mpoexxg  8074  el2mpocsbcl  8082  frxp  8124  xpord2indlem  8145  xpord3inddlem  8152  poseq  8156  smores  8341  naddcllem  8664  naddcom  8671  naddrid  8672  naddunif  8682  naddass  8685  riiner  8790  ixpn0  8937  boxriin  8947  unifi2  9312  wemaplem2  9519  frinsg  9733  rankonidlem  9810  acni3  10050  dfac5  10131  dfac12lem2  10147  kmlem6  10158  kmlem8  10160  kmlem13  10165  cfsmolem  10272  fin23lem40  10353  isf32lem2  10356  fin1a2s  10416  hsmexlem2  10429  hsmex3  10436  axcc4  10441  domtriomlem  10444  dcomex  10449  ac6num  10481  iundom  10550  unirnfdomd  10576  konigthlem  10577  iunctb  10583  gch3  10685  wununi  10715  wunpw  10716  wunpr  10718  eltsk2g  10760  tskpwss  10761  tskpw  10762  grupw  10804  gruurn  10807  intgru  10823  grothpw  10835  grothpwex  10836  grothomex  10838  axgroth3  10840  suplem1pr  11061  supexpr  11063  supsr  11121  fimaxre3  12185  xrsupexmnf  13357  xrinfmexpnf  13358  fsuppmapnn0fiublem  14054  fsuppmapnn0fiub  14055  fsuppmapnn0fiubex  14056  mptnn0fsuppd  14062  rexanre  15434  rexuz3  15436  cau3lem  15442  caubnd2  15445  caubnd  15446  rlim0  15595  rlim0lt  15596  climi2  15598  climi0  15599  climrlim2  15634  rlimres  15645  o1rlimmul  15706  caurcvg  15764  caurcvg2  15765  caucvg  15766  caucvgb  15767  sumeq2  15781  prodeq2  16001  ndvdssub  16499  gcdcllem1  16589  coprmproddvdslem  16752  vdwnnlem1  17087  imasaddfnlem  17614  catidex  17762  catlid  17771  catrid  17772  catcocl  17773  catpropd  17797  subcidcl  17933  funcid  17959  setcepi  18177  tsrss  18677  mgmidmo  18752  mgmidpfod  18770  gsumval2  18788  isnmnd  18840  issubg2  19265  gagrpid  19421  gaass  19424  cygabl  20018  dprdcntz  20137  dprddisj  20138  abveq0  20984  abvmul  20987  abvtri  20988  psgndiflemB  21813  phllmhm  21845  ipcj  21847  ipeq0  21851  mdetmul  22845  pmatcollpw2lem  23002  eltg2b  23184  iincld  23264  iuncld  23270  isclo2  23313  neips  23338  neipeltop  23354  lmcvg  23487  t1t0  23573  hauscmplem  23631  bwth  23635  1stcelcls  23687  ptuni2  23802  pttopon  23822  ptcld  23839  ptcnplem  23847  txtube  23866  txlm  23874  xkococnlem  23885  fbun  24066  isfil2  24082  ptcmplem4  24281  ustssel  24432  isucn2  24504  ucncn  24510  metrest  24750  tngngp  24880  tngngp3  24882  ncvsi  25379  iscau4  25507  cmetcaulem  25516  caussi  25525  volfiniun  25775  iunmbl  25781  voliun  25782  mbfdm  25854  itg2seq  25970  itg2i1fseqle  25982  itg2i1fseq2  25984  iblcnlem  26016  limcresi  26112  limciun  26121  rolle  26217  ulmss  26633  rlimcnp  27202  madebdayim  28153  addsuniflem  28266  oldfib  28642  colinearalg  29367  axpasch  29398  axeuclid  29420  axcontlem2  29422  axcontlem4  29424  axcontlem7  29427  axcontlem8  29428  lfuhgr2  29606  fusgrregdegfi  30029  0grrgr  30040  rusgr1vtxlem  30047  wlkvtxeledg  30083  wlkdlem3  30142  wlkdlem4  30143  lfgriswlk  30150  lfgrwlknloop  30151  eulercrct  30722  1to3vfriendship  30761  frgrregorufr0  30804  isgrpo  30978  grpoidinv  30989  grpoideu  30990  grpoidval  30994  grpoidinv2  30996  vcidOLD  31045  vcdi  31046  vcdir  31047  vcass  31048  nvs  31144  nvz  31150  nvtri  31151  mdbr3  32778  mdbr4  32779  mdsl1i  32802  dmdbr6ati  32904  dmdbr7ati  32905  disjunsn  33067  hasheuni  34595  sigaclcu2  34630  prsiga  34641  measvunilem  34723  cntmeas  34737  omssubadd  34811  signsply0  35059  bnj1498  35570  nummin  35598  axprALT2  35617  tz9.1regs  35660  onvf1odlem4  35703  cvmsdisj  35849  cvmshmeo  35850  cvmliftlem15  35877  cvmlift2lem12  35893  untangtr  36293  elpotr  36358  dfon2lem7  36366  dfon2lem8  36367  nmulprop  36770  opnrebl2  36940  fnemeet2  36986  fnejoin1  36987  fnejoin2  36988  weiunso  37085  weiunse  37087  weiunwe  37088  dfgcd3  38076  domalom  38158  ctbssinf  38160  nlpfvineqsn  38163  fvineqsnf1  38164  pibt1  38170  pibt2  38171  ptrecube  38369  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  poimirlem30  38399  poimirlem31  38400  poimirlem32  38401  heicant  38404  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  frinfm  38485  caushft  38511  sstotbnd3  38526  prdstotbnd  38544  heibor1lem  38559  bfplem2  38573  opidonOLD  38602  exidu1  38606  grpomndo  38625  rngoideu  38653  rngodi  38654  rngodir  38655  rngoass  38656  rngoueqz  38690  idladdcl  38769  idllmulcl  38770  idlrmulcl  38771  mpobi123f  38910  iineq12f  38912  mptbi12f  38914  dmqsblocks  39715  pmapglbx  40642  ltrnnid  41009  cdlemefrs32fva  41273  unitscyglem3  43063  fsuppind  43436  dffltz  43480  lerabdioph  43646  ltrabdioph  43649  nerabdioph  43650  dvdsrabdioph  43651  rencldnfi  43662  dford3  43869  pwelg  44400  pwinfi2  44402  ss2iundf  44499  neik0imk0p  44876  gneispace  44974  gneispace0nelrn  44980  ismnushort  45125  ralbidar  45268  rexbidar  45269  ssclaxsep  45805  uniclaxun  45809  uzubico2  46398  climuzlem  46571  xlimxrre  46659  2reuimp0  48002  bgoldbtbndlem2  48722  bgoldbtbndlem4  48724  mpoexxg2  49268  iuneqconst2  49751  iineqconst2  49752  iunord  50602