Theorem ralimi 3104

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

Syntax hints:   → wi 4   ∈ wcel 2050  ∀wral 3082

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

This theorem depends on definitions:  df-bi 199  df-ral 3087

This theorem is referenced by:  2ralimi  3105  r19.26  3114  r19.29  3194  r19.30  3273  r19.35  3276  rr19.3v  3569  rr19.28v  3570  reu3  3624  uniiunlem  3945  reupick2  4170  uniss2  4740  ss2iun  4805  iineq2  4807  iunss2  4835  disjss2  4896  disjeq2  4897  triin  5041  reusv2lem5  5152  dmmptg  5932  wfisg  6018  fununi  6259  fnmptf  6311  fnmpt  6315  mpteqb  6611  chfnrn  6642  fvn0ssdmfun  6665  dffo5  6691  ffvresb  6709  fmptcof  6713  mpo2eqb  7097  ralrnmpo  7103  abnexg  7293  tfis  7383  fun11uni  7450  fun11iun  7456  zfrep6  7466  mpoexxg  7579  el2mpocsbcl  7586  frxp  7623  smores  7791  riiner  8168  ixpn0  8289  boxriin  8299  unifi2  8607  wemaplem2  8804  rankonidlem  9049  acni3  9265  dfac5  9346  dfac12lem2  9362  kmlem6  9373  kmlem8  9375  kmlem13  9380  cfsmolem  9488  fin23lem40  9569  isf32lem2  9572  fin1a2s  9632  hsmexlem2  9645  hsmex3  9652  axcc4  9657  domtriomlem  9660  dcomex  9665  ac6num  9697  iundom  9760  unirnfdomd  9785  konigthlem  9786  iunctb  9792  gch3  9894  wununi  9924  wunpw  9925  wunpr  9927  eltsk2g  9969  tskpwss  9970  tskpw  9971  grupw  10013  gruurn  10016  intgru  10032  grothpw  10044  grothpwex  10045  grothomex  10047  axgroth3  10049  suplem1pr  10270  supexpr  10272  supsr  10330  fimaxre3  11386  xrsupexmnf  12512  xrinfmexpnf  12513  fsuppmapnn0fiublem  13171  fsuppmapnn0fiub  13172  fsuppmapnn0fiubex  13173  mptnn0fsuppd  13179  rexanre  14565  rexuz3  14567  cau3lem  14573  caubnd2  14576  caubnd  14577  rlim0  14724  rlim0lt  14725  climi2  14727  climi0  14728  climrlim2  14763  rlimres  14774  o1rlimmul  14834  caurcvg  14892  caurcvg2  14893  caucvg  14894  caucvgb  14895  sumeq2  14909  prodeq2  15126  ndvdssub  15618  gcdcllem1  15706  coprmproddvdslem  15860  vdwnnlem1  16185  imasaddfnlem  16655  catidex  16815  catlid  16824  catrid  16825  catcocl  16826  catpropd  16849  subcidcl  16984  funcid  17010  setcepi  17218  tsrss  17703  mgmidmo  17739  gsumval2  17760  isnmnd  17778  issubg2  18090  gagrpid  18207  gaass  18210  dprdcntz  18892  dprddisj  18893  abveq0  19331  abvmul  19334  abvtri  19335  psgndiflemB  20458  phllmhm  20490  ipcj  20492  ipeq0  20496  mdetmul  20948  pmatcollpw2lem  21101  eltg2b  21283  iincld  21363  iuncld  21369  isclo2  21412  neips  21437  neipeltop  21453  lmcvg  21586  t1t0  21672  hauscmplem  21730  bwth  21734  1stcelcls  21785  ptuni2  21900  pttopon  21920  ptcld  21937  ptcnplem  21945  txtube  21964  txlm  21972  xkococnlem  21983  fbun  22164  isfil2  22180  ptcmplem4  22379  ustssel  22529  isucn2  22603  ucncn  22609  metrest  22849  tngngp  22978  tngngp3  22980  ncvsi  23470  iscau4  23597  cmetcaulem  23606  caussi  23615  volfiniun  23863  iunmbl  23869  voliun  23870  mbfdm  23942  itg2seq  24058  itg2i1fseqle  24070  itg2i1fseq2  24072  iblcnlem  24104  limcresi  24198  limciun  24207  rolle  24302  ulmss  24700  rlimcnp  25257  colinearalg  26411  axpasch  26442  axeuclid  26464  axcontlem2  26466  axcontlem4  26468  axcontlem7  26471  axcontlem8  26472  fusgrregdegfi  27066  0grrgr  27077  rusgr1vtxlem  27084  wlkvtxeledg  27120  wlkdlem3  27184  wlkdlem4  27185  lfgriswlk  27188  lfgrwlknloop  27189  eulercrct  27784  1to3vfriendship  27827  frgrregorufr0  27870  isgrpo  28063  grpoidinv  28074  grpoideu  28075  grpoidval  28079  grpoidinv2  28081  vcidOLD  28130  vcdi  28131  vcdir  28132  vcass  28133  nvs  28229  nvz  28235  nvtri  28236  mdbr3  29867  mdbr4  29868  mdsl1i  29891  dmdbr6ati  29993  dmdbr7ati  29994  disjunsn  30124  hasheuni  31017  sigaclcu2  31053  prsiga  31064  measvunilem  31145  cntmeas  31159  omssubadd  31232  signsply0  31496  bnj1498  32007  cvmsdisj  32131  cvmshmeo  32132  cvmliftlem15  32159  cvmlift2lem12  32175  untangtr  32489  elpotr  32575  dfon2lem7  32583  dfon2lem8  32584  tfisg  32605  frpoinsg  32631  frinsg  32637  poseq  32645  opnrebl2  33219  fnemeet2  33265  fnejoin1  33266  fnejoin2  33267  dfgcd3  34076  domalom  34155  ctbssinf  34157  nlpfvineqsn  34160  fvineqsnf1  34161  pibt1  34167  pibt2  34168  ptrecube  34362  poimirlem25  34387  poimirlem26  34388  poimirlem27  34389  poimirlem30  34392  poimirlem31  34393  poimirlem32  34394  heicant  34397  ovoliunnfl  34404  voliunnfl  34406  volsupnfl  34407  frinfm  34481  caushft  34507  sstotbnd3  34525  prdstotbnd  34543  heibor1lem  34558  bfplem2  34572  opidonOLD  34601  exidu1  34605  grpomndo  34624  rngoideu  34652  rngodi  34653  rngodir  34654  rngoass  34655  rngoueqz  34689  idladdcl  34768  idllmulcl  34769  idlrmulcl  34770  mpobi123f  34913  iineq12f  34915  mptbi12f  34917  pmapglbx  36379  ltrnnid  36746  cdlemefrs32fva  37010  dffltz  38707  lerabdioph  38827  ltrabdioph  38830  nerabdioph  38831  dvdsrabdioph  38832  rencldnfi  38843  dford3  39050  pwelg  39310  pwinfi2  39312  ss2iundf  39396  neik0imk0p  39778  gneispace  39876  gneispace0nelrn  39882  ralbidar  40225  rexbidar  40226  uzubico2  41302  climuzlem  41480  xlimxrre  41568  2reuimp0  42744  bgoldbtbndlem2  43364  bgoldbtbndlem4  43366  mpoexxg2  43775  iunord  44171