Theorem ralimi 3160

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

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

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

This theorem depends on definitions:  df-bi 209  df-ral 3143

This theorem is referenced by:  2ralimi  3161  r19.26  3170  r19.29  3254  r19.30  3338  r19.35  3341  rr19.3v  3661  rr19.28v  3662  reu3  3718  uniiunlem  4061  reupick2  4289  uniss2  4871  ss2iun  4937  iineq2  4939  iunss2  4973  disjss2  5034  disjeq2  5035  triin  5187  reusv2lem5  5303  dmmptg  6096  wfisg  6183  fununi  6429  fnmptf  6484  fnmpt  6488  mpteqb  6787  chfnrn  6819  fvn0ssdmfun  6842  dffo5  6870  ffvresb  6888  fmptcof  6892  mpo2eqb  7283  ralrnmpo  7289  abnexg  7478  tfis  7569  fun11uni  7637  fiun  7644  f1iun  7645  zfrep6  7656  mpoexxg  7773  el2mpocsbcl  7780  frxp  7820  smores  7989  riiner  8370  ixpn0  8494  boxriin  8504  unifi2  8814  wemaplem2  9011  rankonidlem  9257  acni3  9473  dfac5  9554  dfac12lem2  9570  kmlem6  9581  kmlem8  9583  kmlem13  9588  cfsmolem  9692  fin23lem40  9773  isf32lem2  9776  fin1a2s  9836  hsmexlem2  9849  hsmex3  9856  axcc4  9861  domtriomlem  9864  dcomex  9869  ac6num  9901  iundom  9964  unirnfdomd  9989  konigthlem  9990  iunctb  9996  gch3  10098  wununi  10128  wunpw  10129  wunpr  10131  eltsk2g  10173  tskpwss  10174  tskpw  10175  grupw  10217  gruurn  10220  intgru  10236  grothpw  10248  grothpwex  10249  grothomex  10251  axgroth3  10253  suplem1pr  10474  supexpr  10476  supsr  10534  fimaxre3  11587  xrsupexmnf  12699  xrinfmexpnf  12700  fsuppmapnn0fiublem  13359  fsuppmapnn0fiub  13360  fsuppmapnn0fiubex  13361  mptnn0fsuppd  13367  rexanre  14706  rexuz3  14708  cau3lem  14714  caubnd2  14717  caubnd  14718  rlim0  14865  rlim0lt  14866  climi2  14868  climi0  14869  climrlim2  14904  rlimres  14915  o1rlimmul  14975  caurcvg  15033  caurcvg2  15034  caucvg  15035  caucvgb  15036  sumeq2  15051  prodeq2  15268  ndvdssub  15760  gcdcllem1  15848  coprmproddvdslem  16006  vdwnnlem1  16331  imasaddfnlem  16801  catidex  16945  catlid  16954  catrid  16955  catcocl  16956  catpropd  16979  subcidcl  17114  funcid  17140  setcepi  17348  tsrss  17833  mgmidmo  17870  gsumval2  17896  isnmnd  17915  issubg2  18294  gagrpid  18424  gaass  18427  cygabl  19010  dprdcntz  19130  dprddisj  19131  abveq0  19597  abvmul  19600  abvtri  19601  psgndiflemB  20744  phllmhm  20776  ipcj  20778  ipeq0  20782  mdetmul  21232  pmatcollpw2lem  21385  eltg2b  21567  iincld  21647  iuncld  21653  isclo2  21696  neips  21721  neipeltop  21737  lmcvg  21870  t1t0  21956  hauscmplem  22014  bwth  22018  1stcelcls  22069  ptuni2  22184  pttopon  22204  ptcld  22221  ptcnplem  22229  txtube  22248  txlm  22256  xkococnlem  22267  fbun  22448  isfil2  22464  ptcmplem4  22663  ustssel  22814  isucn2  22888  ucncn  22894  metrest  23134  tngngp  23263  tngngp3  23265  ncvsi  23755  iscau4  23882  cmetcaulem  23891  caussi  23900  volfiniun  24148  iunmbl  24154  voliun  24155  mbfdm  24227  itg2seq  24343  itg2i1fseqle  24355  itg2i1fseq2  24357  iblcnlem  24389  limcresi  24483  limciun  24492  rolle  24587  ulmss  24985  rlimcnp  25543  colinearalg  26696  axpasch  26727  axeuclid  26749  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  fusgrregdegfi  27351  0grrgr  27362  rusgr1vtxlem  27369  wlkvtxeledg  27405  wlkdlem3  27466  wlkdlem4  27467  lfgriswlk  27470  lfgrwlknloop  27471  eulercrct  28021  1to3vfriendship  28060  frgrregorufr0  28103  isgrpo  28274  grpoidinv  28285  grpoideu  28286  grpoidval  28290  grpoidinv2  28292  vcidOLD  28341  vcdi  28342  vcdir  28343  vcass  28344  nvs  28440  nvz  28446  nvtri  28447  mdbr3  30074  mdbr4  30075  mdsl1i  30098  dmdbr6ati  30200  dmdbr7ati  30201  disjunsn  30344  hasheuni  31344  sigaclcu2  31379  prsiga  31390  measvunilem  31471  cntmeas  31485  omssubadd  31558  signsply0  31821  bnj1498  32333  lfuhgr2  32365  cvmsdisj  32517  cvmshmeo  32518  cvmliftlem15  32545  cvmlift2lem12  32561  untangtr  32940  elpotr  33026  dfon2lem7  33034  dfon2lem8  33035  tfisg  33055  frpoinsg  33081  frinsg  33087  poseq  33095  opnrebl2  33669  fnemeet2  33715  fnejoin1  33716  fnejoin2  33717  dfgcd3  34608  domalom  34688  ctbssinf  34690  nlpfvineqsn  34693  fvineqsnf1  34694  pibt1  34700  pibt2  34701  ptrecube  34907  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  heicant  34942  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  frinfm  35025  caushft  35051  sstotbnd3  35069  prdstotbnd  35087  heibor1lem  35102  bfplem2  35116  opidonOLD  35145  exidu1  35149  grpomndo  35168  rngoideu  35196  rngodi  35197  rngodir  35198  rngoass  35199  rngoueqz  35233  idladdcl  35312  idllmulcl  35313  idlrmulcl  35314  mpobi123f  35455  iineq12f  35457  mptbi12f  35459  pmapglbx  36920  ltrnnid  37287  cdlemefrs32fva  37551  dffltz  39320  lerabdioph  39451  ltrabdioph  39454  nerabdioph  39455  dvdsrabdioph  39456  rencldnfi  39467  dford3  39674  pwelg  39968  pwinfi2  39970  ss2iundf  40053  neik0imk0p  40435  gneispace  40533  gneispace0nelrn  40539  ralbidar  40826  rexbidar  40827  uzubico2  41895  climuzlem  42073  xlimxrre  42161  2reuimp0  43362  bgoldbtbndlem2  44020  bgoldbtbndlem4  44022  mpoexxg2  44435  iunord  44828