Theorem alimi 1813

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 1812	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2		alimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1799	1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-gen 1797  ax-4 1811

This theorem is referenced by:  2alimi  1814  ala1  1815  sylg  1825  19.38  1841  19.26  1872  19.33  1886  alcomimw  2045  hba1w  2051  hbalw  2053  exexw  2055  naev2  2065  2stdpc4  2076  spsbbi  2079  hbal  2173  hbsbwOLD  2178  nfim1  2207  axc4  2327  axc16i  2441  sb4a  2485  dfmoeu  2536  nexmo  2542  eu6  2575  darii  2666  cesare  2673  camestres  2674  festino  2675  baroco  2677  darapti  2685  calemes  2688  fesapo  2692  eqeq1d  2739  ralimi2  3070  rgen2a  3343  rmoeq1  3383  ceqsal1t  3475  spcgft  3508  vtoclgft  3511  rspct  3564  elabgt  3628  elabgtOLD  3629  elabgtOLDOLD  3630  reu6  3686  sbciegftOLD  3780  csbeq2  3856  ssrmof  4003  ralss  4010  rabss2OLD  4032  csbnestgfw  4376  csbnestgf  4381  undif4  4421  rzal  4449  falseral0OLD  4470  ralidmw  4471  ralidm  4472  intmin4  4934  dfiin2g  4988  invdisj  5086  disjss3  5099  axrep2  5229  sepex  5247  ax6vsep  5250  axnul  5252  csbexg  5257  axpow3  5315  nfnid  5322  axprALT  5369  axprlem1  5370  axprlem4  5373  axprlem4OLD  5376  axprlem5OLD  5377  axprOLD  5378  axprg  5383  ssrelrel  5753  iresn0n0  6021  iotanul  6480  iota4  6481  fundif  6549  fv3  6860  zfrep6  7909  ssfi  9109  elirrv  9514  dfom3  9568  dfac5  10051  dfac2a  10052  dfac2b  10053  kmlem13  10085  zorng  10426  brdom3  10450  brdom4  10452  axpowndlem2  10521  axregnd  10527  axacndlem1  10530  axacndlem2  10531  axacndlem3  10532  axacndlem4  10533  axacnd  10535  ingru  10738  dfnn2  12170  trclfvcotr  14944  prodeq2w  15845  2ndcdisj2  23413  elons2  28266  dfn0s2  28340  pjnormssi  32255  disjin  32672  disjin2  32673  ssdifidlprm  33550  bnj1172  35176  bnj1174  35178  bnj1176  35180  bnj1523  35246  axsepg2  35257  axsepg2ALT  35258  r1omhfb  35287  fineqvpow  35290  r1omhfbregs  35312  elpotr  35992  dfon2lem8  36001  distel  36014  hbimtg  36017  mh-setindnd  36686  bj-gl4  36816  bj-almpi  36834  bj-alanim  36838  bj-2albi  36839  bj-exim  36854  bj-aleximiALT  36856  bj-exalim  36861  bj-cbvalimt  36869  bj-cbveximt  36870  bj-cbvaw  36878  bj-cbveaw  36880  bj-ssbid2ALT  36902  bj-sb  36926  bj-hbext  36949  bj-nfalt  36950  bj-nfext  36951  bj-nnfbd0  36983  bj-nnfalt  37022  bj-nnfext  37023  bj-cbv3tb  37029  bj-nfs1t2  37033  bj-hbaeb2  37060  bj-equsal1  37066  bj-equsal2  37067  2stdpc5  37071  bj-ceqsalt0  37126  bj-ceqsalt1  37127  bj-abv  37148  bj-bm1.3ii  37306  bj-axnul  37314  bj-rep  37315  exrecfnlem  37628  wl-moae  37765  wl-aleq  37784  wl-sb8ft  37799  wl-sb8eft  37800  wl-lem-nexmo  37816  wl-axc11rc11  37832  phpreu  37849  nninfnub  37996  mpobi123f  38407  eqab2  38495  trcoss  38817  hba1-o  39267  aecom-o  39271  ax12fromc15  39275  hbequid  39279  axc711  39284  axc711toc7  39286  axc711to11  39287  axc5c711  39288  axc5c711toc7  39290  axc5c711to11  39291  equidqe  39292  equid1ALT  39295  axc11nfromc11  39296  axc11n-16  39308  ax12eq  39311  ax12el  39312  ax12indi  39314  eu6w  43028  dfac11  43413  intimag  44006  intimasn  44007  frege70  44283  pm11.12  44725  2albi  44728  2exbi  44730  pm11.57  44739  pm11.61  44743  axc5c4c711toc7  44754  axc5c4c711to11  44755  axc11next  44756  pm13.192  44760  ralbidar  44794  rexbidar  44795  hbntal  44903  hbimpg  44904  hbexg  44906  ax6e2nd  44908  hbimpgVD  45253  ax6e2eqVD  45256  ax6e2ndVD  45257  ax6e2ndALT  45279  ssclaxsep  45332  absnsb  47381  rexrsb  47454  ichal  47820  setrec1lem2  50041  setrec1lem4  50043