Theorem ralimi 3067

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3045

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

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

This theorem is referenced by:  rexbi  3087  ralrexbid  3088  r19.35OLD  3090  r19.26  3092  r19.29OLD  3096  r19.30  3101  2ralimi  3104  3ralimi  3105  4ralimi  3106  5ralimi  3107  6ralimi  3108  r19.21v  3159  rr19.3v  3636  rr19.28v  3637  reu3  3701  uniiunlem  4053  reupick2  4297  ralf0  4480  uniss2  4908  ss2iun  4977  iineq2  4979  dfiun2g  4997  iunss2  5016  disjss2  5080  disjeq2  5081  triin  5234  reusv2lem5  5360  dmmptg  6218  frpoinsg  6319  fununi  6594  fnmptf  6657  fnmpt  6661  mpteqb  6990  chfnrn  7024  fvn0ssdmfun  7049  dffo5  7079  ffvresb  7100  fmptcof  7105  mpo2eqb  7524  ralrnmpo  7531  abnexg  7735  tfisg  7833  tfis  7834  fun11uni  7912  fiun  7924  f1iun  7925  zfrep6  7936  mpoexxg  8057  el2mpocsbcl  8067  frxp  8108  xpord2indlem  8129  xpord3inddlem  8136  poseq  8140  smores  8324  naddcllem  8643  naddcom  8649  naddrid  8650  naddunif  8660  naddass  8663  riiner  8766  ixpn0  8906  boxriin  8916  unifi2  9303  wemaplem2  9507  frinsg  9711  rankonidlem  9788  acni3  10007  dfac5  10089  dfac12lem2  10105  kmlem6  10116  kmlem8  10118  kmlem13  10123  cfsmolem  10230  fin23lem40  10311  isf32lem2  10314  fin1a2s  10374  hsmexlem2  10387  hsmex3  10394  axcc4  10399  domtriomlem  10402  dcomex  10407  ac6num  10439  iundom  10502  unirnfdomd  10527  konigthlem  10528  iunctb  10534  gch3  10636  wununi  10666  wunpw  10667  wunpr  10669  eltsk2g  10711  tskpwss  10712  tskpw  10713  grupw  10755  gruurn  10758  intgru  10774  grothpw  10786  grothpwex  10787  grothomex  10789  axgroth3  10791  suplem1pr  11012  supexpr  11014  supsr  11072  fimaxre3  12136  xrsupexmnf  13272  xrinfmexpnf  13273  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  fsuppmapnn0fiubex  13964  mptnn0fsuppd  13970  rexanre  15320  rexuz3  15322  cau3lem  15328  caubnd2  15331  caubnd  15332  rlim0  15481  rlim0lt  15482  climi2  15484  climi0  15485  climrlim2  15520  rlimres  15531  o1rlimmul  15592  caurcvg  15650  caurcvg2  15651  caucvg  15652  caucvgb  15653  sumeq2  15667  prodeq2  15885  ndvdssub  16386  gcdcllem1  16476  coprmproddvdslem  16639  vdwnnlem1  16973  imasaddfnlem  17498  catidex  17642  catlid  17651  catrid  17652  catcocl  17653  catpropd  17677  subcidcl  17813  funcid  17839  setcepi  18057  tsrss  18555  mgmidmo  18594  gsumval2  18620  isnmnd  18672  issubg2  19080  gagrpid  19233  gaass  19236  cygabl  19828  dprdcntz  19947  dprddisj  19948  abveq0  20734  abvmul  20737  abvtri  20738  psgndiflemB  21516  phllmhm  21548  ipcj  21550  ipeq0  21554  mdetmul  22517  pmatcollpw2lem  22671  eltg2b  22853  iincld  22933  iuncld  22939  isclo2  22982  neips  23007  neipeltop  23023  lmcvg  23156  t1t0  23242  hauscmplem  23300  bwth  23304  1stcelcls  23355  ptuni2  23470  pttopon  23490  ptcld  23507  ptcnplem  23515  txtube  23534  txlm  23542  xkococnlem  23553  fbun  23734  isfil2  23750  ptcmplem4  23949  ustssel  24100  isucn2  24173  ucncn  24179  metrest  24419  tngngp  24549  tngngp3  24551  ncvsi  25058  iscau4  25186  cmetcaulem  25195  caussi  25204  volfiniun  25455  iunmbl  25461  voliun  25462  mbfdm  25534  itg2seq  25650  itg2i1fseqle  25662  itg2i1fseq2  25664  iblcnlem  25697  limcresi  25793  limciun  25802  rolle  25901  ulmss  26313  rlimcnp  26882  madebdayim  27806  addsuniflem  27915  colinearalg  28844  axpasch  28875  axeuclid  28897  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  fusgrregdegfi  29504  0grrgr  29515  rusgr1vtxlem  29522  wlkvtxeledg  29559  wlkdlem3  29619  wlkdlem4  29620  lfgriswlk  29623  lfgrwlknloop  29624  eulercrct  30178  1to3vfriendship  30217  frgrregorufr0  30260  isgrpo  30433  grpoidinv  30444  grpoideu  30445  grpoidval  30449  grpoidinv2  30451  vcidOLD  30500  vcdi  30501  vcdir  30502  vcass  30503  nvs  30599  nvz  30605  nvtri  30606  mdbr3  32233  mdbr4  32234  mdsl1i  32257  dmdbr6ati  32359  dmdbr7ati  32360  disjunsn  32530  hasheuni  34082  sigaclcu2  34117  prsiga  34128  measvunilem  34209  cntmeas  34223  omssubadd  34298  signsply0  34549  bnj1498  35058  nummin  35088  onvf1odlem4  35100  lfuhgr2  35113  cvmsdisj  35264  cvmshmeo  35265  cvmliftlem15  35292  cvmlift2lem12  35308  untangtr  35708  elpotr  35776  dfon2lem7  35784  dfon2lem8  35785  opnrebl2  36316  fnemeet2  36362  fnejoin1  36363  fnejoin2  36364  weiunso  36461  weiunse  36463  weiunwe  36464  dfgcd3  37319  domalom  37399  ctbssinf  37401  nlpfvineqsn  37404  fvineqsnf1  37405  pibt1  37411  pibt2  37412  ptrecube  37621  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  heicant  37656  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  frinfm  37736  caushft  37762  sstotbnd3  37777  prdstotbnd  37795  heibor1lem  37810  bfplem2  37824  opidonOLD  37853  exidu1  37857  grpomndo  37876  rngoideu  37904  rngodi  37905  rngodir  37906  rngoass  37907  rngoueqz  37941  idladdcl  38020  idllmulcl  38021  idlrmulcl  38022  mpobi123f  38163  iineq12f  38165  mptbi12f  38167  dmqsblocks  38852  pmapglbx  39770  ltrnnid  40137  cdlemefrs32fva  40401  unitscyglem3  42192  fsuppind  42585  dffltz  42629  lerabdioph  42800  ltrabdioph  42803  nerabdioph  42804  dvdsrabdioph  42805  rencldnfi  42816  dford3  43024  pwelg  43556  pwinfi2  43558  ss2iundf  43655  neik0imk0p  44032  gneispace  44130  gneispace0nelrn  44136  ismnushort  44297  ralbidar  44441  rexbidar  44442  ssclaxsep  44979  uniclaxun  44983  uzubico2  45573  climuzlem  45748  xlimxrre  45836  natlocalincr  46881  2reuimp0  47119  bgoldbtbndlem2  47811  bgoldbtbndlem4  47813  mpoexxg2  48330  iuneqconst2  48815  iineqconst2  48816  iunord  49669