Theorem alimi 1844

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-gen 1828  ax-4 1842

This theorem is used by:  2alimi  1845  ala1  1846  sylg  1856  19.38  1872  19.26  1903  19.33  1917  alcomimw  2076  hba1w  2082  hbalw  2084  exexw  2086  naev2  2096  2stdpc4  2107  spsbbi  2110  hbal  2204  nfim1  2236  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  3095  rgen2a  3357  rmoeq1  3397  ceqsal1t  3483  spcgft  3513  vtoclgft  3516  rspct  3563  elabgt  3626  elabgtOLD  3627  reu6  3684  csbeq2  3852  ssrmof  3999  ralss  4004  rabss2OLD  4026  csbnestgfw  4380  csbnestgf  4385  undif4  4420  rzal  4450  falseral0OLD  4471  ralidmw  4472  ralidm  4473  intmin4  4937  dfiin2g  4989  invdisj  5089  disjss3  5102  axrep2  5235  replem  5241  zfrep6  5242  sepex  5255  ax6vsep  5257  axnul  5259  csbexg  5264  axpow3  5330  nfnid  5337  axprALT  5384  axprlem1  5385  axprlem4  5388  axprlem1OLD  5390  axprg  5395  ssrelrel  5772  iresn0n0  6048  iotanul  6511  iota4  6512  fundif  6581  fv3  6895  zfrep6OLD  7956  ssfi  9172  elirrvOLD  9576  dfom3  9632  setrec1lem2  9948  setrec1lem4  9952  dfac5  10188  dfac2a  10189  dfac2b  10190  kmlem13  10222  zorng  10563  brdom3  10588  brdom4  10590  axpowndlem2  10664  axregnd  10670  axacndlem1  10673  axacndlem2  10674  axacndlem3  10675  axacndlem4  10676  axacnd  10678  ingru  10881  dfnn2  12329  trclfvcotr  15142  prodeq2w  16059  ssdifidlprm  21622  2ndcdisj2  23756  elons2  28626  dfn0s2  28700  pjnormssi  32752  disjin  33162  disjin2  33163  bnj1172  35614  bnj1174  35616  bnj1176  35618  bnj1523  35684  axprALT2  35713  r1omhfb  35717  fineqvpow  35756  r1omhfbregs  35778  axsepg2  35781  axsepg3  35782  axsepg3ALT  35783  axsepg4  35784  axpowg2  35788  axpowg3  35789  elpotr  36513  dfon2lem8  36522  distel  36535  hbimtg  36538  axtco1from2  37233  axtcond  37236  mh-setindnd  37295  bj-gl4  37435  bj-almpi  37459  bj-alanim  37467  bj-2albi  37468  bj-exim  37479  bj-aleximiALT  37481  bj-exalim  37484  bj-cbvaw  37510  bj-cbveaw  37512  bj-ssbid2ALT  37532  bj-sb  37559  bj-nfalt  37585  bj-nfext  37586  bj-nnfbd0  37620  bj-nnfalt  37662  bj-nnfext  37663  bj-cbv3tb  37669  bj-nfs1t2  37673  bj-hbaeb2  37700  bj-equsal1  37706  bj-equsal2  37707  2stdpc5  37711  bj-ceqsalt0  37766  bj-ceqsalt1  37767  bj-abv  37788  bj-bm1.3ii  37947  bj-axnul  37956  bj-rep  37957  exrecfnlem  38270  wl-dfcleq  38405  wl-moae  38416  wl-aleq  38435  wl-sb8ft  38450  wl-sb8eft  38451  wl-lem-nexmo  38467  wl-axc11rc11  38483  phpreu  38495  findcard4  38600  nninfnub  38653  mpobi123f  39062  eqab2  39150  trcoss  39472  hba1-o  39922  aecom-o  39926  ax12fromc15  39930  hbequid  39934  axc711  39939  axc711toc7  39941  axc711to11  39942  axc5c711  39943  axc5c711toc7  39945  axc5c711to11  39946  equidqe  39947  equid1ALT  39950  axc11nfromc11  39951  axc11n-16  39963  ax12eq  39966  ax12el  39967  ax12indi  39969  eu6w  43641  dfac11  44022  intimag  44615  intimasn  44616  frege70  44892  pm11.12  45318  2albi  45321  2exbi  45323  pm11.57  45332  pm11.61  45336  axc5c4c711toc7  45347  axc5c4c711to11  45348  axc11next  45349  pm13.192  45353  ralbidar  45387  rexbidar  45388  hbntal  45495  hbimpg  45496  hbexg  45498  ax6e2nd  45500  hbimpgVD  45845  ax6e2eqVD  45848  ax6e2ndVD  45849  ax6e2ndALT  45871  ssclaxsep  45924  quantgodelALT  47829  absnsb  48041  rexrsb  48114  ichal  48492