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  2326  axc16i  2440  sb4a  2484  dfmoeu  2535  nexmo  2541  eu6  2574  darii  2665  cesare  2672  camestres  2673  festino  2674  baroco  2676  darapti  2684  calemes  2687  fesapo  2691  eqeq1d  2738  ralimi2  3069  rgen2a  3333  rmoeq1  3373  ceqsal1t  3462  spcgft  3494  vtoclgft  3497  rspct  3550  elabgt  3614  elabgtOLD  3615  elabgtOLDOLD  3616  reu6  3672  sbciegftOLD  3766  csbeq2  3842  ssrmof  3989  ralss  3996  rabss2OLD  4018  csbnestgfw  4362  csbnestgf  4367  undif4  4407  rzal  4434  falseral0OLD  4455  ralidmw  4456  ralidm  4457  intmin4  4919  dfiin2g  4973  invdisj  5071  disjss3  5084  axrep2  5215  replem  5223  zfrep6  5224  sepex  5235  ax6vsep  5238  axnul  5240  csbexg  5245  axpow3  5310  nfnid  5317  axprALT  5364  axprlem1  5365  axprlem4  5368  axprlem1OLD  5370  axprlem4OLD  5372  axprlem5OLD  5373  axprOLD  5374  axprg  5379  ssrelrel  5752  iresn0n0  6019  iotanul  6478  iota4  6479  fundif  6547  fv3  6858  zfrep6OLD  7908  ssfi  9107  elirrv  9512  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  12187  trclfvcotr  14971  prodeq2w  15875  2ndcdisj2  23422  elons2  28250  dfn0s2  28324  pjnormssi  32239  disjin  32656  disjin2  32657  ssdifidlprm  33518  bnj1172  35143  bnj1174  35145  bnj1176  35147  bnj1523  35213  axsepg2  35225  axsepg2ALT  35226  axprALT2  35253  r1omhfb  35256  fineqvpow  35259  r1omhfbregs  35281  elpotr  35961  dfon2lem8  35970  distel  35983  hbimtg  35986  axtco1from2  36657  axtcond  36660  mh-setindnd  36719  bj-gl4  36860  bj-almpi  36884  bj-alanim  36892  bj-2albi  36893  bj-exim  36904  bj-aleximiALT  36906  bj-exalim  36909  bj-cbvaw  36935  bj-cbveaw  36937  bj-ssbid2ALT  36957  bj-sb  36984  bj-nfalt  37010  bj-nfext  37011  bj-nnfbd0  37045  bj-nnfalt  37087  bj-nnfext  37088  bj-cbv3tb  37094  bj-nfs1t2  37098  bj-hbaeb2  37125  bj-equsal1  37131  bj-equsal2  37132  2stdpc5  37136  bj-ceqsalt0  37191  bj-ceqsalt1  37192  bj-abv  37213  bj-bm1.3ii  37371  bj-axnul  37379  bj-rep  37380  exrecfnlem  37695  wl-dfcleq  37830  wl-moae  37841  wl-aleq  37860  wl-sb8ft  37875  wl-sb8eft  37876  wl-lem-nexmo  37892  wl-axc11rc11  37908  phpreu  37925  nninfnub  38072  mpobi123f  38483  eqab2  38571  trcoss  38893  hba1-o  39343  aecom-o  39347  ax12fromc15  39351  hbequid  39355  axc711  39360  axc711toc7  39362  axc711to11  39363  axc5c711  39364  axc5c711toc7  39366  axc5c711to11  39367  equidqe  39368  equid1ALT  39371  axc11nfromc11  39372  axc11n-16  39384  ax12eq  39387  ax12el  39388  ax12indi  39390  eu6w  43109  dfac11  43490  intimag  44083  intimasn  44084  frege70  44360  pm11.12  44802  2albi  44805  2exbi  44807  pm11.57  44816  pm11.61  44820  axc5c4c711toc7  44831  axc5c4c711to11  44832  axc11next  44833  pm13.192  44837  ralbidar  44871  rexbidar  44872  hbntal  44980  hbimpg  44981  hbexg  44983  ax6e2nd  44985  hbimpgVD  45330  ax6e2eqVD  45333  ax6e2ndVD  45334  ax6e2ndALT  45356  ssclaxsep  45409  quantgodelALT  47303  absnsb  47475  rexrsb  47548  ichal  47926  setrec1lem2  50163  setrec1lem4  50165