Theorem ralimi 3084

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3062

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 3063

This theorem is referenced by:  rexbi  3105  ralrexbid  3107  r19.35OLD  3110  r19.26  3112  r19.29OLD  3116  r19.30  3121  r19.30OLD  3122  2ralimi  3124  3ralimi  3125  4ralimi  3126  5ralimi  3127  6ralimi  3128  r19.21v  3180  rr19.3v  3658  rr19.28v  3659  reu3  3724  uniiunlem  4085  reupick2  4321  ralf0  4514  uniss2  4946  ss2iun  5016  iineq2  5018  dfiun2g  5034  iunss2  5053  disjss2  5117  disjeq2  5118  triin  5283  reusv2lem5  5401  dmmptg  6242  frpoinsg  6345  wfisgOLD  6356  fununi  6624  fnmptf  6687  fnmpt  6691  mpteqb  7018  chfnrn  7051  fvn0ssdmfun  7077  dffo5  7106  ffvresb  7124  fmptcof  7128  mpo2eqb  7541  ralrnmpo  7547  abnexg  7743  tfisg  7843  tfis  7844  fun11uni  7923  fiun  7929  f1iun  7930  zfrep6  7941  mpoexxg  8062  el2mpocsbcl  8071  frxp  8112  xpord2indlem  8133  xpord3inddlem  8140  poseq  8144  smores  8352  naddcllem  8675  naddcom  8681  naddrid  8682  naddunif  8692  naddass  8695  riiner  8784  ixpn0  8924  boxriin  8934  unifi2  9342  wemaplem2  9542  frinsg  9746  rankonidlem  9823  acni3  10042  dfac5  10123  dfac12lem2  10139  kmlem6  10150  kmlem8  10152  kmlem13  10157  cfsmolem  10265  fin23lem40  10346  isf32lem2  10349  fin1a2s  10409  hsmexlem2  10422  hsmex3  10429  axcc4  10434  domtriomlem  10437  dcomex  10442  ac6num  10474  iundom  10537  unirnfdomd  10562  konigthlem  10563  iunctb  10569  gch3  10671  wununi  10701  wunpw  10702  wunpr  10704  eltsk2g  10746  tskpwss  10747  tskpw  10748  grupw  10790  gruurn  10793  intgru  10809  grothpw  10821  grothpwex  10822  grothomex  10824  axgroth3  10826  suplem1pr  11047  supexpr  11049  supsr  11107  fimaxre3  12160  xrsupexmnf  13284  xrinfmexpnf  13285  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0fiubex  13957  mptnn0fsuppd  13963  rexanre  15293  rexuz3  15295  cau3lem  15301  caubnd2  15304  caubnd  15305  rlim0  15452  rlim0lt  15453  climi2  15455  climi0  15456  climrlim2  15491  rlimres  15502  o1rlimmul  15563  caurcvg  15623  caurcvg2  15624  caucvg  15625  caucvgb  15626  sumeq2  15640  prodeq2  15858  ndvdssub  16352  gcdcllem1  16440  coprmproddvdslem  16599  vdwnnlem1  16928  imasaddfnlem  17474  catidex  17618  catlid  17627  catrid  17628  catcocl  17629  catpropd  17653  subcidcl  17794  funcid  17820  setcepi  18038  tsrss  18542  mgmidmo  18579  gsumval2  18605  isnmnd  18629  issubg2  19021  gagrpid  19158  gaass  19161  cygabl  19759  dprdcntz  19878  dprddisj  19879  abveq0  20434  abvmul  20437  abvtri  20438  psgndiflemB  21153  phllmhm  21185  ipcj  21187  ipeq0  21191  mdetmul  22125  pmatcollpw2lem  22279  eltg2b  22462  iincld  22543  iuncld  22549  isclo2  22592  neips  22617  neipeltop  22633  lmcvg  22766  t1t0  22852  hauscmplem  22910  bwth  22914  1stcelcls  22965  ptuni2  23080  pttopon  23100  ptcld  23117  ptcnplem  23125  txtube  23144  txlm  23152  xkococnlem  23163  fbun  23344  isfil2  23360  ptcmplem4  23559  ustssel  23710  isucn2  23784  ucncn  23790  metrest  24033  tngngp  24171  tngngp3  24173  ncvsi  24668  iscau4  24796  cmetcaulem  24805  caussi  24814  volfiniun  25064  iunmbl  25070  voliun  25071  mbfdm  25143  itg2seq  25260  itg2i1fseqle  25272  itg2i1fseq2  25274  iblcnlem  25306  limcresi  25402  limciun  25411  rolle  25507  ulmss  25909  rlimcnp  26470  madebdayim  27383  addsuniflem  27487  colinearalg  28199  axpasch  28230  axeuclid  28252  axcontlem2  28254  axcontlem4  28256  axcontlem7  28259  axcontlem8  28260  fusgrregdegfi  28857  0grrgr  28868  rusgr1vtxlem  28875  wlkvtxeledg  28912  wlkdlem3  28972  wlkdlem4  28973  lfgriswlk  28976  lfgrwlknloop  28977  eulercrct  29526  1to3vfriendship  29565  frgrregorufr0  29608  isgrpo  29781  grpoidinv  29792  grpoideu  29793  grpoidval  29797  grpoidinv2  29799  vcidOLD  29848  vcdi  29849  vcdir  29850  vcass  29851  nvs  29947  nvz  29953  nvtri  29954  mdbr3  31581  mdbr4  31582  mdsl1i  31605  dmdbr6ati  31707  dmdbr7ati  31708  disjunsn  31856  hasheuni  33114  sigaclcu2  33149  prsiga  33160  measvunilem  33241  cntmeas  33255  omssubadd  33330  signsply0  33593  bnj1498  34103  nummin  34125  lfuhgr2  34140  cvmsdisj  34292  cvmshmeo  34293  cvmliftlem15  34320  cvmlift2lem12  34336  untangtr  34714  elpotr  34784  dfon2lem7  34792  dfon2lem8  34793  opnrebl2  35254  fnemeet2  35300  fnejoin1  35301  fnejoin2  35302  dfgcd3  36253  domalom  36333  ctbssinf  36335  nlpfvineqsn  36338  fvineqsnf1  36339  pibt1  36345  pibt2  36346  ptrecube  36536  poimirlem25  36561  poimirlem26  36562  poimirlem27  36563  poimirlem30  36566  poimirlem31  36567  poimirlem32  36568  heicant  36571  ovoliunnfl  36578  voliunnfl  36580  volsupnfl  36581  frinfm  36651  caushft  36677  sstotbnd3  36692  prdstotbnd  36710  heibor1lem  36725  bfplem2  36739  opidonOLD  36768  exidu1  36772  grpomndo  36791  rngoideu  36819  rngodi  36820  rngodir  36821  rngoass  36822  rngoueqz  36856  idladdcl  36935  idllmulcl  36936  idlrmulcl  36937  mpobi123f  37078  iineq12f  37080  mptbi12f  37082  pmapglbx  38688  ltrnnid  39055  cdlemefrs32fva  39319  fsuppind  41210  dffltz  41424  lerabdioph  41591  ltrabdioph  41594  nerabdioph  41595  dvdsrabdioph  41596  rencldnfi  41607  dford3  41815  pwelg  42359  pwinfi2  42361  ss2iundf  42458  neik0imk0p  42835  gneispace  42933  gneispace0nelrn  42939  ismnushort  43108  ralbidar  43252  rexbidar  43253  uzubico2  44331  climuzlem  44507  xlimxrre  44595  natlocalincr  45638  2reuimp0  45870  bgoldbtbndlem2  46522  bgoldbtbndlem4  46524  mpoexxg2  47061  iunord  47769