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  2434  sb4a  2478  dfmoeu  2529  nexmo  2534  moimi  2538  eu6  2567  darii  2658  cesare  2665  camestres  2666  festino  2667  baroco  2669  darapti  2677  calemes  2680  fesapo  2684  eqeq1d  2731  ralimi2  3061  rgen2a  3345  rmoeq1  3387  ceqsal1t  3480  spcgft  3515  vtoclgft  3518  rspct  3574  elabgt  3638  elabgtOLD  3639  elabgtOLDOLD  3640  reu6  3697  sbciegftOLD  3791  csbeq2  3867  ssrmof  4014  ralss  4021  rabss2  4041  csbnestgfw  4385  csbnestgf  4390  undif4  4430  ralidmw  4471  ralidm  4475  ralf0  4477  falseral0  4479  intmin4  4941  dfiin2g  4996  invdisj  5093  disjss3  5106  axrep2  5237  sepex  5255  ax6vsep  5258  axnul  5260  csbexg  5265  axpow3  5323  nfnid  5330  axprALT  5377  axprlem1  5378  axprlem4  5381  axprlem4OLD  5384  axprlem5OLD  5385  axprOLD  5386  ssrelrel  5759  iresn0n0  6025  iotanul  6489  iota4  6492  fundif  6565  fv3  6876  zfrep6  7933  ssfi  9137  dfom3  9600  dfac5  10082  dfac2a  10083  dfac2b  10084  kmlem13  10116  zorng  10457  brdom3  10481  brdom4  10483  axpowndlem2  10551  axregnd  10557  axacndlem1  10560  axacndlem2  10561  axacndlem3  10562  axacndlem4  10563  axacnd  10565  ingru  10768  dfnn2  12199  trclfvcotr  14975  prodeq2w  15876  2ndcdisj2  23344  elons2  28159  dfn0s2  28224  pjnormssi  32097  disjin  32515  disjin2  32516  ssdifidlprm  33429  bnj1172  34991  bnj1174  34993  bnj1176  34995  bnj1523  35061  axsepg2  35072  axsepg2ALT  35073  fineqvpow  35086  elpotr  35769  dfon2lem8  35778  distel  35791  hbimtg  35794  bj-gl4  36583  bj-alanim  36600  bj-2albi  36601  bj-exalim  36620  bj-cbvalimt  36627  bj-cbveximt  36628  bj-eximALT  36629  bj-aleximiALT  36630  bj-ssbid2ALT  36651  bj-sb  36675  bj-hbext  36698  bj-nfalt  36699  bj-nfext  36700  bj-nnfalt  36754  bj-nnfext  36755  bj-cbv3tb  36775  bj-nfs1t2  36779  bj-hbaeb2  36806  bj-equsal1  36812  bj-equsal2  36813  2stdpc5  36817  bj-ceqsalt0  36872  bj-ceqsalt1  36873  bj-abv  36894  bj-bm1.3ii  37052  exrecfnlem  37367  wl-moae  37504  wl-aleq  37523  wl-sb8ft  37538  wl-sb8eft  37539  wl-lem-nexmo  37555  wl-axc11rc11  37571  phpreu  37598  nninfnub  37745  mpobi123f  38156  eqab2  38237  trcoss  38473  hba1-o  38890  aecom-o  38894  ax12fromc15  38898  hbequid  38902  axc711  38907  axc711toc7  38909  axc711to11  38910  axc5c711  38911  axc5c711toc7  38913  axc5c711to11  38914  equidqe  38915  equid1ALT  38918  axc11nfromc11  38919  axc11n-16  38931  ax12eq  38934  ax12el  38935  ax12indi  38937  eu6w  42664  dfac11  43051  intimag  43645  intimasn  43646  frege70  43922  pm11.12  44364  2albi  44367  2exbi  44369  pm11.57  44378  pm11.61  44382  axc5c4c711toc7  44393  axc5c4c711to11  44394  axc11next  44395  pm13.192  44399  ralbidar  44434  rexbidar  44435  hbntal  44543  hbimpg  44544  hbexg  44546  ax6e2nd  44548  hbimpgVD  44893  ax6e2eqVD  44896  ax6e2ndVD  44897  ax6e2ndALT  44919  ssclaxsep  44972  absnsb  47025  rexrsb  47098  ichal  47464  setrec1lem2  49674  setrec1lem4  49676