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  6040  iotanul  6497  iota4  6498  fundif  6566  fv3  6881  zfrep6OLD  7932  ssfi  9137  elirrvOLD  9543  dfom3  9599  dfac5  10082  dfac2a  10083  dfac2b  10084  kmlem13  10116  zorng  10458  brdom3  10482  brdom4  10484  axpowndlem2  10553  axregnd  10559  axacndlem1  10562  axacndlem2  10563  axacndlem3  10564  axacndlem4  10565  axacnd  10567  ingru  10770  dfnn2  12220  trclfvcotr  15019  prodeq2w  15923  2ndcdisj2  23497  elons2  28328  dfn0s2  28402  pjnormssi  32317  disjin  32735  disjin2  32736  ssdifidlprm  33606  bnj1172  35260  bnj1174  35262  bnj1176  35264  bnj1523  35330  axprALT2  35369  r1omhfb  35372  fineqvpow  35375  r1omhfbregs  35397  axsepg2  35400  axsepg3  35401  axsepg3ALT  35402  axsepg4  35403  axpowg2  35407  axpowg3  35408  elpotr  36093  dfon2lem8  36102  distel  36115  hbimtg  36118  axtco1from2  36799  axtcond  36802  mh-setindnd  36861  bj-gl4  37002  bj-almpi  37026  bj-alanim  37034  bj-2albi  37035  bj-exim  37046  bj-aleximiALT  37048  bj-exalim  37051  bj-cbvaw  37077  bj-cbveaw  37079  bj-ssbid2ALT  37099  bj-sb  37126  bj-nfalt  37152  bj-nfext  37153  bj-nnfbd0  37187  bj-nnfalt  37229  bj-nnfext  37230  bj-cbv3tb  37236  bj-nfs1t2  37240  bj-hbaeb2  37267  bj-equsal1  37273  bj-equsal2  37274  2stdpc5  37278  bj-ceqsalt0  37333  bj-ceqsalt1  37334  bj-abv  37355  bj-bm1.3ii  37513  bj-axnul  37521  bj-rep  37522  exrecfnlem  37837  wl-dfcleq  37972  wl-moae  37983  wl-aleq  38002  wl-sb8ft  38017  wl-sb8eft  38018  wl-lem-nexmo  38034  wl-axc11rc11  38050  phpreu  38067  nninfnub  38214  mpobi123f  38625  eqab2  38713  trcoss  39035  hba1-o  39485  aecom-o  39489  ax12fromc15  39493  hbequid  39497  axc711  39502  axc711toc7  39504  axc711to11  39505  axc5c711  39506  axc5c711toc7  39508  axc5c711to11  39509  equidqe  39510  equid1ALT  39513  axc11nfromc11  39514  axc11n-16  39526  ax12eq  39529  ax12el  39530  ax12indi  39532  eu6w  43222  dfac11  43603  intimag  44196  intimasn  44197  frege70  44473  pm11.12  44915  2albi  44918  2exbi  44920  pm11.57  44929  pm11.61  44933  axc5c4c711toc7  44944  axc5c4c711to11  44945  axc11next  44946  pm13.192  44950  ralbidar  44984  rexbidar  44985  hbntal  45093  hbimpg  45094  hbexg  45096  ax6e2nd  45098  hbimpgVD  45443  ax6e2eqVD  45446  ax6e2ndVD  45447  ax6e2ndALT  45469  ssclaxsep  45522  quantgodelALT  47413  absnsb  47585  rexrsb  47658  ichal  48036  setrec1lem2  50273  setrec1lem4  50275