Theorem alimi 1841

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

Syntax hints:   → wi 4  ∀wal 1568

This theorem was proved from axioms:  ax-mp 5  ax-gen 1825  ax-4 1839

This theorem is referenced by:  2alimi  1842  ala1  1843  sylg  1853  19.38  1869  19.26  1900  19.33  1914  alcomimw  2073  hba1w  2079  hbalw  2081  exexw  2083  naev2  2093  2stdpc4  2104  spsbbi  2107  hbal  2202  nfim1  2235  axc4  2354  axc16i  2468  sb4a  2512  dfmoeu  2563  nexmo  2569  eu6  2602  darii  2692  cesare  2699  camestres  2700  festino  2701  baroco  2703  darapti  2711  calemes  2714  fesapo  2718  eqeq1d  2765  ralimi2  3097  rgen2a  3360  rmoeq1  3400  ceqsal1t  3487  spcgft  3518  vtoclgft  3521  rspct  3568  elabgt  3632  elabgtOLD  3633  reu6  3690  csbeq2  3859  ssrmof  4006  ralss  4011  rabss2OLD  4033  csbnestgfw  4388  csbnestgf  4393  undif4  4428  rzal  4456  falseral0OLD  4477  ralidmw  4478  ralidm  4479  intmin4  4943  dfiin2g  4996  invdisj  5096  disjss3  5109  axrep2  5242  replem  5250  zfrep6  5251  sepex  5264  ax6vsep  5267  axnul  5269  csbexg  5274  axpow3  5341  nfnid  5348  axprALT  5395  axprlem1  5396  axprlem4  5399  axprlem1OLD  5401  axprlem4OLD  5403  axprlem5OLD  5404  axprOLD  5405  axprg  5410  ssrelrel  5784  iresn0n0  6058  iotanul  6518  iota4  6519  fundif  6587  fv3  6901  zfrep6OLD  7953  ssfi  9158  elirrvOLD  9561  dfom3  9617  dfac5  10113  dfac2a  10114  dfac2b  10115  kmlem13  10147  zorng  10489  brdom3  10513  brdom4  10515  axpowndlem2  10584  axregnd  10590  axacndlem1  10593  axacndlem2  10594  axacndlem3  10595  axacndlem4  10596  axacnd  10598  ingru  10801  dfnn2  12247  trclfvcotr  15048  prodeq2w  15966  ssdifidlprm  21467  2ndcdisj2  23595  elons2  28432  dfn0s2  28506  pjnormssi  32501  disjin  32912  disjin2  32913  bnj1172  35370  bnj1174  35372  bnj1176  35374  bnj1523  35440  axprALT2  35484  r1omhfb  35489  fineqvpow  35509  r1omhfbregs  35531  axsepg2  35534  axsepg3  35535  axsepg3ALT  35536  axsepg4  35537  axpowg2  35541  axpowg3  35542  elpotr  36252  dfon2lem8  36261  distel  36274  hbimtg  36277  axtco1from2  36967  axtcond  36970  mh-setindnd  37029  bj-gl4  37169  bj-almpi  37193  bj-alanim  37201  bj-2albi  37202  bj-exim  37213  bj-aleximiALT  37215  bj-exalim  37218  bj-cbvaw  37244  bj-cbveaw  37246  bj-ssbid2ALT  37266  bj-sb  37293  bj-nfalt  37319  bj-nfext  37320  bj-nnfbd0  37354  bj-nnfalt  37396  bj-nnfext  37397  bj-cbv3tb  37403  bj-nfs1t2  37407  bj-hbaeb2  37434  bj-equsal1  37440  bj-equsal2  37441  2stdpc5  37445  bj-ceqsalt0  37500  bj-ceqsalt1  37501  bj-abv  37522  bj-bm1.3ii  37681  bj-axnul  37690  bj-rep  37691  exrecfnlem  38006  wl-dfcleq  38141  wl-moae  38152  wl-aleq  38171  wl-sb8ft  38186  wl-sb8eft  38187  wl-lem-nexmo  38203  wl-axc11rc11  38219  phpreu  38236  nninfnub  38383  mpobi123f  38792  eqab2  38880  trcoss  39202  hba1-o  39652  aecom-o  39656  ax12fromc15  39660  hbequid  39664  axc711  39669  axc711toc7  39671  axc711to11  39672  axc5c711  39673  axc5c711toc7  39675  axc5c711to11  39676  equidqe  39677  equid1ALT  39680  axc11nfromc11  39681  axc11n-16  39693  ax12eq  39696  ax12el  39697  ax12indi  39699  eu6w  43391  dfac11  43772  intimag  44365  intimasn  44366  frege70  44642  pm11.12  45068  2albi  45071  2exbi  45073  pm11.57  45082  pm11.61  45086  axc5c4c711toc7  45097  axc5c4c711to11  45098  axc11next  45099  pm13.192  45103  ralbidar  45137  rexbidar  45138  hbntal  45245  hbimpg  45246  hbexg  45248  ax6e2nd  45250  hbimpgVD  45595  ax6e2eqVD  45598  ax6e2ndVD  45599  ax6e2ndALT  45621  ssclaxsep  45674  quantgodelALT  47572  absnsb  47747  rexrsb  47820  ichal  48198  setrec1lem2  50449  setrec1lem4  50451