Theorem ralimi 3087

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3064

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

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

This theorem is referenced by:  2ralimi  3088  r19.26  3095  r19.21v  3113  rexbi  3173  r19.29  3184  ralrexbid  3255  r19.30  3268  r19.30OLD  3269  r19.35  3271  rr19.3v  3598  rr19.28v  3599  reu3  3662  uniiunlem  4019  reupick2  4254  ralf0  4444  uniss2  4874  ss2iun  4942  iineq2  4944  dfiun2g  4960  iunss2  4979  disjss2  5042  disjeq2  5043  triin  5206  reusv2lem5  5325  dmmptg  6145  frpoinsg  6246  wfisgOLD  6257  fununi  6509  fnmptf  6569  fnmpt  6573  mpteqb  6894  chfnrn  6926  fvn0ssdmfun  6952  dffo5  6980  ffvresb  6998  fmptcof  7002  mpo2eqb  7406  ralrnmpo  7412  abnexg  7606  tfis  7701  fun11uni  7779  fiun  7785  f1iun  7786  zfrep6  7797  mpoexxg  7916  el2mpocsbcl  7925  frxp  7967  smores  8183  riiner  8579  ixpn0  8718  boxriin  8728  unifi2  9109  wemaplem2  9306  frinsg  9509  rankonidlem  9586  acni3  9803  dfac5  9884  dfac12lem2  9900  kmlem6  9911  kmlem8  9913  kmlem13  9918  cfsmolem  10026  fin23lem40  10107  isf32lem2  10110  fin1a2s  10170  hsmexlem2  10183  hsmex3  10190  axcc4  10195  domtriomlem  10198  dcomex  10203  ac6num  10235  iundom  10298  unirnfdomd  10323  konigthlem  10324  iunctb  10330  gch3  10432  wununi  10462  wunpw  10463  wunpr  10465  eltsk2g  10507  tskpwss  10508  tskpw  10509  grupw  10551  gruurn  10554  intgru  10570  grothpw  10582  grothpwex  10583  grothomex  10585  axgroth3  10587  suplem1pr  10808  supexpr  10810  supsr  10868  fimaxre3  11921  xrsupexmnf  13039  xrinfmexpnf  13040  fsuppmapnn0fiublem  13710  fsuppmapnn0fiub  13711  fsuppmapnn0fiubex  13712  mptnn0fsuppd  13718  rexanre  15058  rexuz3  15060  cau3lem  15066  caubnd2  15069  caubnd  15070  rlim0  15217  rlim0lt  15218  climi2  15220  climi0  15221  climrlim2  15256  rlimres  15267  o1rlimmul  15328  caurcvg  15388  caurcvg2  15389  caucvg  15390  caucvgb  15391  sumeq2  15406  prodeq2  15624  ndvdssub  16118  gcdcllem1  16206  coprmproddvdslem  16367  vdwnnlem1  16696  imasaddfnlem  17239  catidex  17383  catlid  17392  catrid  17393  catcocl  17394  catpropd  17418  subcidcl  17559  funcid  17585  setcepi  17803  tsrss  18307  mgmidmo  18344  gsumval2  18370  isnmnd  18389  issubg2  18770  gagrpid  18900  gaass  18903  cygabl  19491  dprdcntz  19611  dprddisj  19612  abveq0  20086  abvmul  20089  abvtri  20090  psgndiflemB  20805  phllmhm  20837  ipcj  20839  ipeq0  20843  mdetmul  21772  pmatcollpw2lem  21926  eltg2b  22109  iincld  22190  iuncld  22196  isclo2  22239  neips  22264  neipeltop  22280  lmcvg  22413  t1t0  22499  hauscmplem  22557  bwth  22561  1stcelcls  22612  ptuni2  22727  pttopon  22747  ptcld  22764  ptcnplem  22772  txtube  22791  txlm  22799  xkococnlem  22810  fbun  22991  isfil2  23007  ptcmplem4  23206  ustssel  23357  isucn2  23431  ucncn  23437  metrest  23680  tngngp  23818  tngngp3  23820  ncvsi  24315  iscau4  24443  cmetcaulem  24452  caussi  24461  volfiniun  24711  iunmbl  24717  voliun  24718  mbfdm  24790  itg2seq  24907  itg2i1fseqle  24919  itg2i1fseq2  24921  iblcnlem  24953  limcresi  25049  limciun  25058  rolle  25154  ulmss  25556  rlimcnp  26115  colinearalg  27278  axpasch  27309  axeuclid  27331  axcontlem2  27333  axcontlem4  27335  axcontlem7  27338  axcontlem8  27339  fusgrregdegfi  27936  0grrgr  27947  rusgr1vtxlem  27954  wlkvtxeledg  27991  wlkdlem3  28052  wlkdlem4  28053  lfgriswlk  28056  lfgrwlknloop  28057  eulercrct  28606  1to3vfriendship  28645  frgrregorufr0  28688  isgrpo  28859  grpoidinv  28870  grpoideu  28871  grpoidval  28875  grpoidinv2  28877  vcidOLD  28926  vcdi  28927  vcdir  28928  vcass  28929  nvs  29025  nvz  29031  nvtri  29032  mdbr3  30659  mdbr4  30660  mdsl1i  30683  dmdbr6ati  30785  dmdbr7ati  30786  disjunsn  30933  hasheuni  32053  sigaclcu2  32088  prsiga  32099  measvunilem  32180  cntmeas  32194  omssubadd  32267  signsply0  32530  bnj1498  33041  nummin  33063  lfuhgr2  33080  cvmsdisj  33232  cvmshmeo  33233  cvmliftlem15  33260  cvmlift2lem12  33276  untangtr  33655  elpotr  33757  dfon2lem7  33765  dfon2lem8  33766  tfisg  33786  xpord2ind  33794  xpord3ind  33800  poseq  33802  naddcllem  33831  naddcom  33835  naddid1  33836  madebdayim  34070  opnrebl2  34510  fnemeet2  34556  fnejoin1  34557  fnejoin2  34558  dfgcd3  35495  domalom  35575  ctbssinf  35577  nlpfvineqsn  35580  fvineqsnf1  35581  pibt1  35587  pibt2  35588  ptrecube  35777  poimirlem25  35802  poimirlem26  35803  poimirlem27  35804  poimirlem30  35807  poimirlem31  35808  poimirlem32  35809  heicant  35812  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  frinfm  35893  caushft  35919  sstotbnd3  35934  prdstotbnd  35952  heibor1lem  35967  bfplem2  35981  opidonOLD  36010  exidu1  36014  grpomndo  36033  rngoideu  36061  rngodi  36062  rngodir  36063  rngoass  36064  rngoueqz  36098  idladdcl  36177  idllmulcl  36178  idlrmulcl  36179  mpobi123f  36320  iineq12f  36322  mptbi12f  36324  pmapglbx  37783  ltrnnid  38150  cdlemefrs32fva  38414  fsuppind  40279  dffltz  40471  lerabdioph  40627  ltrabdioph  40630  nerabdioph  40631  dvdsrabdioph  40632  rencldnfi  40643  dford3  40850  pwelg  41167  pwinfi2  41169  ss2iundf  41267  neik0imk0p  41646  gneispace  41744  gneispace0nelrn  41750  ismnushort  41919  ralbidar  42063  rexbidar  42064  uzubico2  43108  climuzlem  43284  xlimxrre  43372  2reuimp0  44606  bgoldbtbndlem2  45258  bgoldbtbndlem4  45260  mpoexxg2  45673  iunord  46382  natlocalincr  46511