Theorem ralimi 3074

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

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

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 3052

This theorem is referenced by:  rexbi  3093  ralrexbid  3094  r19.26  3097  r19.30  3104  2ralimi  3107  3ralimi  3108  4ralimi  3109  5ralimi  3110  6ralimi  3111  r19.21v  3162  rr19.3v  3609  rr19.28v  3610  reu3  3673  uniiunlem  4027  reupick2  4271  uniss2  4884  ss2iun  4952  iineq2  4954  dfiun2g  4972  iunss2  4992  disjss2  5055  disjeq2  5056  triin  5209  replem  5223  zfrep6  5224  reusv2lem5  5344  dmmptg  6206  frpoinsg  6307  fununi  6573  fnmptf  6634  fnmpt  6638  mpteqb  6967  chfnrn  7001  fvn0ssdmfun  7026  dffo5  7056  ffvresb  7078  fmptcof  7083  mpo2eqb  7499  ralrnmpo  7506  abnexg  7710  tfisg  7805  tfis  7806  fun11uni  7884  fiun  7896  f1iun  7897  zfrep6OLD  7908  mpoexxg  8028  el2mpocsbcl  8035  frxp  8076  xpord2indlem  8097  xpord3inddlem  8104  poseq  8108  smores  8292  naddcllem  8612  naddcom  8618  naddrid  8619  naddunif  8629  naddass  8632  riiner  8737  ixpn0  8878  boxriin  8888  unifi2  9255  wemaplem2  9462  frinsg  9675  rankonidlem  9752  acni3  9969  dfac5  10051  dfac12lem2  10067  kmlem6  10078  kmlem8  10080  kmlem13  10085  cfsmolem  10192  fin23lem40  10273  isf32lem2  10276  fin1a2s  10336  hsmexlem2  10349  hsmex3  10356  axcc4  10361  domtriomlem  10364  dcomex  10369  ac6num  10401  iundom  10464  unirnfdomd  10490  konigthlem  10491  iunctb  10497  gch3  10599  wununi  10629  wunpw  10630  wunpr  10632  eltsk2g  10674  tskpwss  10675  tskpw  10676  grupw  10718  gruurn  10721  intgru  10737  grothpw  10749  grothpwex  10750  grothomex  10752  axgroth3  10754  suplem1pr  10975  supexpr  10977  supsr  11035  fimaxre3  12102  xrsupexmnf  13257  xrinfmexpnf  13258  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  fsuppmapnn0fiubex  13954  mptnn0fsuppd  13960  rexanre  15309  rexuz3  15311  cau3lem  15317  caubnd2  15320  caubnd  15321  rlim0  15470  rlim0lt  15471  climi2  15473  climi0  15474  climrlim2  15509  rlimres  15520  o1rlimmul  15581  caurcvg  15639  caurcvg2  15640  caucvg  15641  caucvgb  15642  sumeq2  15656  prodeq2  15877  ndvdssub  16378  gcdcllem1  16468  coprmproddvdslem  16631  vdwnnlem1  16966  imasaddfnlem  17492  catidex  17640  catlid  17649  catrid  17650  catcocl  17651  catpropd  17675  subcidcl  17811  funcid  17837  setcepi  18055  tsrss  18555  mgmidmo  18628  gsumval2  18654  isnmnd  18706  issubg2  19117  gagrpid  19269  gaass  19272  cygabl  19866  dprdcntz  19985  dprddisj  19986  abveq0  20795  abvmul  20798  abvtri  20799  psgndiflemB  21580  phllmhm  21612  ipcj  21614  ipeq0  21618  mdetmul  22588  pmatcollpw2lem  22742  eltg2b  22924  iincld  23004  iuncld  23010  isclo2  23053  neips  23078  neipeltop  23094  lmcvg  23227  t1t0  23313  hauscmplem  23371  bwth  23375  1stcelcls  23426  ptuni2  23541  pttopon  23561  ptcld  23578  ptcnplem  23586  txtube  23605  txlm  23613  xkococnlem  23624  fbun  23805  isfil2  23821  ptcmplem4  24020  ustssel  24171  isucn2  24243  ucncn  24249  metrest  24489  tngngp  24619  tngngp3  24621  ncvsi  25118  iscau4  25246  cmetcaulem  25255  caussi  25264  volfiniun  25514  iunmbl  25520  voliun  25521  mbfdm  25593  itg2seq  25709  itg2i1fseqle  25721  itg2i1fseq2  25723  iblcnlem  25756  limcresi  25852  limciun  25861  rolle  25957  ulmss  26362  rlimcnp  26929  madebdayim  27880  addsuniflem  27993  oldfib  28369  colinearalg  28979  axpasch  29010  axeuclid  29032  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  fusgrregdegfi  29638  0grrgr  29649  rusgr1vtxlem  29656  wlkvtxeledg  29692  wlkdlem3  29751  wlkdlem4  29752  lfgriswlk  29755  lfgrwlknloop  29756  eulercrct  30312  1to3vfriendship  30351  frgrregorufr0  30394  isgrpo  30568  grpoidinv  30579  grpoideu  30580  grpoidval  30584  grpoidinv2  30586  vcidOLD  30635  vcdi  30636  vcdir  30637  vcass  30638  nvs  30734  nvz  30740  nvtri  30741  mdbr3  32368  mdbr4  32369  mdsl1i  32392  dmdbr6ati  32494  dmdbr7ati  32495  disjunsn  32664  hasheuni  34229  sigaclcu2  34264  prsiga  34275  measvunilem  34356  cntmeas  34370  omssubadd  34444  signsply0  34695  bnj1498  35203  nummin  35236  axprALT2  35253  tz9.1regs  35278  onvf1odlem4  35288  lfuhgr2  35301  cvmsdisj  35452  cvmshmeo  35453  cvmliftlem15  35480  cvmlift2lem12  35496  untangtr  35896  elpotr  35961  dfon2lem7  35969  dfon2lem8  35970  opnrebl2  36503  fnemeet2  36549  fnejoin1  36550  fnejoin2  36551  weiunso  36648  weiunse  36650  weiunwe  36651  dfgcd3  37638  domalom  37720  ctbssinf  37722  nlpfvineqsn  37725  fvineqsnf1  37726  pibt1  37732  pibt2  37733  ptrecube  37941  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  heicant  37976  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  frinfm  38056  caushft  38082  sstotbnd3  38097  prdstotbnd  38115  heibor1lem  38130  bfplem2  38144  opidonOLD  38173  exidu1  38177  grpomndo  38196  rngoideu  38224  rngodi  38225  rngodir  38226  rngoass  38227  rngoueqz  38261  idladdcl  38340  idllmulcl  38341  idlrmulcl  38342  mpobi123f  38483  iineq12f  38485  mptbi12f  38487  dmqsblocks  39288  pmapglbx  40215  ltrnnid  40582  cdlemefrs32fva  40846  unitscyglem3  42636  fsuppind  43023  dffltz  43067  lerabdioph  43233  ltrabdioph  43236  nerabdioph  43237  dvdsrabdioph  43238  rencldnfi  43249  dford3  43456  pwelg  43987  pwinfi2  43989  ss2iundf  44086  neik0imk0p  44463  gneispace  44561  gneispace0nelrn  44567  ismnushort  44728  ralbidar  44871  rexbidar  44872  ssclaxsep  45409  uniclaxun  45413  uzubico2  45998  climuzlem  46171  xlimxrre  46259  natlocalincr  47306  2reuimp0  47562  bgoldbtbndlem2  48282  bgoldbtbndlem4  48284  mpoexxg2  48814  iuneqconst2  49298  iineqconst2  49299  iunord  50151