Theorem alimi 1830

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

Syntax hints:   → wi 4  ∀wal 1557

This theorem was proved from axioms:  ax-mp 5  ax-gen 1814  ax-4 1828

This theorem is referenced by:  2alimi  1831  ala1  1832  sylg  1842  19.38  1858  19.26  1889  19.33  1903  alcomimw  2062  hba1w  2068  hbalw  2070  exexw  2072  naev2  2082  2stdpc4  2100  spsbbi  2105  hbal  2200  nfim1  2233  axc4  2352  axc16i  2466  sb4a  2510  dfmoeu  2561  nexmo  2567  eu6  2600  darii  2690  cesare  2697  camestres  2698  festino  2699  baroco  2701  darapti  2709  calemes  2712  fesapo  2716  eqeq1d  2763  ralimi2  3093  rgen2a  3357  rmoeq1  3397  ceqsal1t  3485  spcgft  3516  vtoclgft  3519  rspct  3567  elabgt  3631  elabgtOLD  3632  reu6  3688  csbeq2  3857  ssrmof  4004  ralss  4009  rabss2OLD  4031  csbnestgfw  4375  csbnestgf  4380  undif4  4420  rzal  4447  falseral0OLD  4468  ralidmw  4469  ralidm  4470  intmin4  4934  dfiin2g  4987  invdisj  5085  disjss3  5098  axrep2  5229  replem  5237  zfrep6  5238  sepex  5249  ax6vsep  5252  axnul  5254  csbexg  5259  axpow3  5324  nfnid  5331  axprALT  5378  axprlem1  5379  axprlem4  5382  axprlem1OLD  5384  axprlem4OLD  5386  axprlem5OLD  5387  axprOLD  5388  axprg  5393  ssrelrel  5766  iresn0n0  6038  iotanul  6495  iota4  6496  fundif  6564  fv3  6879  zfrep6OLD  7930  ssfi  9135  elirrvOLD  9541  dfom3  9597  dfac5  10080  dfac2a  10081  dfac2b  10082  kmlem13  10114  zorng  10456  brdom3  10480  brdom4  10482  axpowndlem2  10551  axregnd  10557  axacndlem1  10560  axacndlem2  10561  axacndlem3  10562  axacndlem4  10563  axacnd  10565  ingru  10768  dfnn2  12218  trclfvcotr  15017  prodeq2w  15921  2ndcdisj2  23495  elons2  28326  dfn0s2  28400  pjnormssi  32315  disjin  32733  disjin2  32734  ssdifidlprm  33604  bnj1172  35258  bnj1174  35260  bnj1176  35262  bnj1523  35328  axprALT2  35365  r1omhfb  35368  fineqvpow  35371  r1omhfbregs  35393  axsepg2  35396  axsepg3  35397  axsepg3ALT  35398  axsepg4  35399  axpowg2  35403  axpowg3  35404  elpotr  36082  dfon2lem8  36091  distel  36104  hbimtg  36107  axtco1from2  36788  axtcond  36791  mh-setindnd  36850  bj-gl4  36991  bj-almpi  37015  bj-alanim  37023  bj-2albi  37024  bj-exim  37035  bj-aleximiALT  37037  bj-exalim  37040  bj-cbvaw  37066  bj-cbveaw  37068  bj-ssbid2ALT  37088  bj-sb  37115  bj-nfalt  37141  bj-nfext  37142  bj-nnfbd0  37176  bj-nnfalt  37218  bj-nnfext  37219  bj-cbv3tb  37225  bj-nfs1t2  37229  bj-hbaeb2  37256  bj-equsal1  37262  bj-equsal2  37263  2stdpc5  37267  bj-ceqsalt0  37322  bj-ceqsalt1  37323  bj-abv  37344  bj-bm1.3ii  37502  bj-axnul  37510  bj-rep  37511  exrecfnlem  37826  wl-dfcleq  37961  wl-moae  37972  wl-aleq  37991  wl-sb8ft  38006  wl-sb8eft  38007  wl-lem-nexmo  38023  wl-axc11rc11  38039  phpreu  38056  nninfnub  38203  mpobi123f  38614  eqab2  38702  trcoss  39024  hba1-o  39474  aecom-o  39478  ax12fromc15  39482  hbequid  39486  axc711  39491  axc711toc7  39493  axc711to11  39494  axc5c711  39495  axc5c711toc7  39497  axc5c711to11  39498  equidqe  39499  equid1ALT  39502  axc11nfromc11  39503  axc11n-16  39515  ax12eq  39518  ax12el  39519  ax12indi  39521  eu6w  43211  dfac11  43592  intimag  44185  intimasn  44186  frege70  44462  pm11.12  44904  2albi  44907  2exbi  44909  pm11.57  44918  pm11.61  44922  axc5c4c711toc7  44933  axc5c4c711to11  44934  axc11next  44935  pm13.192  44939  ralbidar  44973  rexbidar  44974  hbntal  45082  hbimpg  45083  hbexg  45085  ax6e2nd  45087  hbimpgVD  45432  ax6e2eqVD  45435  ax6e2ndVD  45436  ax6e2ndALT  45458  ssclaxsep  45511  quantgodelALT  47402  absnsb  47574  rexrsb  47647  ichal  48025  setrec1lem2  50262  setrec1lem4  50264