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  3336  rmoeq1  3378  ceqsal1t  3471  spcgft  3506  vtoclgft  3509  rspct  3565  elabgt  3629  elabgtOLD  3630  elabgtOLDOLD  3631  reu6  3688  sbciegftOLD  3782  csbeq2  3858  ssrmof  4005  ralss  4012  rabss2  4031  csbnestgfw  4375  csbnestgf  4380  undif4  4420  ralidmw  4461  ralidm  4465  ralf0  4467  falseral0  4469  intmin4  4930  dfiin2g  4984  invdisj  5081  disjss3  5094  axrep2  5224  sepex  5242  ax6vsep  5245  axnul  5247  csbexg  5252  axpow3  5310  nfnid  5317  axprALT  5364  axprlem1  5365  axprlem4  5368  axprlem4OLD  5371  axprlem5OLD  5372  axprOLD  5373  ssrelrel  5743  iresn0n0  6009  iotanul  6466  iota4  6467  fundif  6535  fv3  6844  zfrep6  7897  ssfi  9097  elirrv  9508  dfom3  9562  dfac5  10042  dfac2a  10043  dfac2b  10044  kmlem13  10076  zorng  10417  brdom3  10441  brdom4  10443  axpowndlem2  10511  axregnd  10517  axacndlem1  10520  axacndlem2  10521  axacndlem3  10522  axacndlem4  10523  axacnd  10525  ingru  10728  dfnn2  12159  trclfvcotr  14934  prodeq2w  15835  2ndcdisj2  23360  elons2  28182  dfn0s2  28247  pjnormssi  32130  disjin  32548  disjin2  32549  ssdifidlprm  33405  bnj1172  34967  bnj1174  34969  bnj1176  34971  bnj1523  35037  axsepg2  35048  axsepg2ALT  35049  fineqvpow  35070  elpotr  35754  dfon2lem8  35763  distel  35776  hbimtg  35779  bj-gl4  36568  bj-alanim  36585  bj-2albi  36586  bj-exalim  36605  bj-cbvalimt  36612  bj-cbveximt  36613  bj-eximALT  36614  bj-aleximiALT  36615  bj-ssbid2ALT  36636  bj-sb  36660  bj-hbext  36683  bj-nfalt  36684  bj-nfext  36685  bj-nnfalt  36739  bj-nnfext  36740  bj-cbv3tb  36760  bj-nfs1t2  36764  bj-hbaeb2  36791  bj-equsal1  36797  bj-equsal2  36798  2stdpc5  36802  bj-ceqsalt0  36857  bj-ceqsalt1  36858  bj-abv  36879  bj-bm1.3ii  37037  exrecfnlem  37352  wl-moae  37489  wl-aleq  37508  wl-sb8ft  37523  wl-sb8eft  37524  wl-lem-nexmo  37540  wl-axc11rc11  37556  phpreu  37583  nninfnub  37730  mpobi123f  38141  eqab2  38222  trcoss  38458  hba1-o  38875  aecom-o  38879  ax12fromc15  38883  hbequid  38887  axc711  38892  axc711toc7  38894  axc711to11  38895  axc5c711  38896  axc5c711toc7  38898  axc5c711to11  38899  equidqe  38900  equid1ALT  38903  axc11nfromc11  38904  axc11n-16  38916  ax12eq  38919  ax12el  38920  ax12indi  38922  eu6w  42649  dfac11  43035  intimag  43629  intimasn  43630  frege70  43906  pm11.12  44348  2albi  44351  2exbi  44353  pm11.57  44362  pm11.61  44366  axc5c4c711toc7  44377  axc5c4c711to11  44378  axc11next  44379  pm13.192  44383  ralbidar  44418  rexbidar  44419  hbntal  44527  hbimpg  44528  hbexg  44530  ax6e2nd  44532  hbimpgVD  44877  ax6e2eqVD  44880  ax6e2ndVD  44881  ax6e2ndALT  44903  ssclaxsep  44956  absnsb  47012  rexrsb  47085  ichal  47451  setrec1lem2  49674  setrec1lem4  49676