Theorem alimi 1811

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)

Hypothesis

Ref	Expression
alimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alimi	⊢ (∀𝑥𝜑 → ∀𝑥𝜓)

Proof of Theorem alimi

Step	Hyp	Ref	Expression
1		alim 1810	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2		alimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1797	1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-gen 1795  ax-4 1809

This theorem is referenced by:  2alimi  1812  ala1  1813  sylg  1823  19.38  1839  19.26  1870  19.33  1884  alcomimw  2043  hba1w  2048  hbalw  2050  exexw  2052  naev2  2062  2stdpc4  2071  spsbbi  2074  hbal  2168  hbsbwOLD  2173  nfim1  2200  axc4  2320  axc16i  2435  sb4a  2479  dfmoeu  2530  nexmo  2535  moimi  2539  eu6  2568  darii  2659  cesare  2666  camestres  2667  festino  2668  baroco  2670  darapti  2678  calemes  2681  fesapo  2685  eqeq1d  2732  ralimi2  3062  rgen2a  3347  rmoeq1  3390  ceqsal1t  3483  spcgft  3518  vtoclgft  3521  rspct  3577  elabgt  3641  elabgtOLD  3642  elabgtOLDOLD  3643  reu6  3700  sbciegftOLD  3794  csbeq2  3870  ssrmof  4017  ralss  4024  rabss2  4044  csbnestgfw  4388  csbnestgf  4393  undif4  4433  ralidmw  4474  ralidm  4478  ralf0  4480  falseral0  4482  intmin4  4944  dfiin2g  4999  invdisj  5096  disjss3  5109  axrep2  5240  sepex  5258  ax6vsep  5261  axnul  5263  csbexg  5268  axpow3  5326  nfnid  5333  axprALT  5380  axprlem1  5381  axprlem4  5384  axprlem4OLD  5387  axprlem5OLD  5388  axprOLD  5389  ssrelrel  5762  iresn0n0  6028  iotanul  6492  iota4  6495  fundif  6568  fv3  6879  zfrep6  7936  ssfi  9143  dfom3  9607  dfac5  10089  dfac2a  10090  dfac2b  10091  kmlem13  10123  zorng  10464  brdom3  10488  brdom4  10490  axpowndlem2  10558  axregnd  10564  axacndlem1  10567  axacndlem2  10568  axacndlem3  10569  axacndlem4  10570  axacnd  10572  ingru  10775  dfnn2  12206  trclfvcotr  14982  prodeq2w  15883  2ndcdisj2  23351  elons2  28166  dfn0s2  28231  pjnormssi  32104  disjin  32522  disjin2  32523  ssdifidlprm  33436  bnj1172  34998  bnj1174  35000  bnj1176  35002  bnj1523  35068  axsepg2  35079  axsepg2ALT  35080  fineqvpow  35093  elpotr  35776  dfon2lem8  35785  distel  35798  hbimtg  35801  bj-gl4  36590  bj-alanim  36607  bj-2albi  36608  bj-exalim  36627  bj-cbvalimt  36634  bj-cbveximt  36635  bj-eximALT  36636  bj-aleximiALT  36637  bj-ssbid2ALT  36658  bj-sb  36682  bj-hbext  36705  bj-nfalt  36706  bj-nfext  36707  bj-nnfalt  36761  bj-nnfext  36762  bj-cbv3tb  36782  bj-nfs1t2  36786  bj-hbaeb2  36813  bj-equsal1  36819  bj-equsal2  36820  2stdpc5  36824  bj-ceqsalt0  36879  bj-ceqsalt1  36880  bj-abv  36901  bj-bm1.3ii  37059  exrecfnlem  37374  wl-moae  37511  wl-aleq  37530  wl-sb8ft  37545  wl-sb8eft  37546  wl-lem-nexmo  37562  wl-axc11rc11  37578  phpreu  37605  nninfnub  37752  mpobi123f  38163  eqab2  38244  trcoss  38480  hba1-o  38897  aecom-o  38901  ax12fromc15  38905  hbequid  38909  axc711  38914  axc711toc7  38916  axc711to11  38917  axc5c711  38918  axc5c711toc7  38920  axc5c711to11  38921  equidqe  38922  equid1ALT  38925  axc11nfromc11  38926  axc11n-16  38938  ax12eq  38941  ax12el  38942  ax12indi  38944  eu6w  42671  dfac11  43058  intimag  43652  intimasn  43653  frege70  43929  pm11.12  44371  2albi  44374  2exbi  44376  pm11.57  44385  pm11.61  44389  axc5c4c711toc7  44400  axc5c4c711to11  44401  axc11next  44402  pm13.192  44406  ralbidar  44441  rexbidar  44442  hbntal  44550  hbimpg  44551  hbexg  44553  ax6e2nd  44555  hbimpgVD  44900  ax6e2eqVD  44903  ax6e2ndVD  44904  ax6e2ndALT  44926  ssclaxsep  44979  absnsb  47032  rexrsb  47105  ichal  47471  setrec1lem2  49681  setrec1lem4  49683