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  1919  alcomimw  2078  hba1w  2084  hbalw  2086  exexw  2088  naev2  2098  2stdpc4  2109  spsbbi  2112  hbal  2207  nfim1  2239  axc4  2355  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  3098  rgen2a  3360  rmoeq1  3400  ceqsal1t  3486  spcgft  3516  vtoclgft  3519  rspct  3566  elabgt  3629  elabgtOLD  3630  reu6  3687  csbeq2  3856  ssrmof  3981  ralss  3986  rabss2OLD  4006  csbnestgfw  4383  csbnestgf  4388  undif4  4423  rzal  4453  falseral0OLD  4474  ralidmw  4475  ralidm  4476  intmin4  4940  dfiin2g  4992  invdisj  5092  disjss3  5105  axrep2  5239  replem  5245  zfrep6  5246  sepex  5259  ax6vsep  5261  axnul  5263  csbexg  5268  axpow3  5335  nfnid  5342  axprALT  5389  axprlem1  5390  axprlem4  5393  axprlem1OLD  5395  axprg  5400  ssrelrel  5778  iresn0n0  6059  iotanul  6540  iota4  6541  fundifOLD  6614  fv3  6929  zfrep6OLD  7994  ssfi  9219  elirrvOLD  9622  dfom3  9678  setrec1lem2  9997  setrec1lem4  10001  dfac5  10237  dfac2a  10238  dfac2b  10239  kmlem13  10271  zorng  10612  brdom3  10637  brdom4  10639  axpowndlem2  10713  axregnd  10719  axacndlem1  10722  axacndlem2  10723  axacndlem3  10724  axacndlem4  10725  axacnd  10727  ingru  10930  dfnn2  12378  trclfvcotr  15194  prodeq2w  16111  ssdifidlprm  21675  2ndcdisj2  23809  elons2  28677  dfn0s2  28751  pjnormssi  32803  disjin  33255  disjin2  33256  bnj1172  35714  bnj1174  35716  bnj1176  35718  bnj1523  35784  reu6f  35792  rmo6  35793  axprALT2  35829  eqhf  35833  dfac15  35858  dfac16  35859  fineqvpow  35896  eqhfregs  35918  axsepg2  35921  axsepg3  35922  axsepg3ALT  35923  axsepg4  35924  axpowg2  35928  axpowg3  35929  onprcf1acwevdlem2  36059  elpotr  36734  dfon2lem8  36743  distel  36756  hbimtg  36759  axtco1from2  37454  axtcond  37457  mh-setindnd  37516  bj-gl4  37656  bj-almpi  37680  bj-alanim  37688  bj-2albi  37689  bj-exim  37700  bj-aleximiALT  37702  bj-exalim  37705  bj-cbvaw  37731  bj-cbveaw  37733  bj-ssbid2ALT  37753  bj-sb  37780  bj-nfalt  37806  bj-nfext  37807  bj-nnfbd0  37841  bj-nnfalt  37883  bj-nnfext  37884  bj-cbv3tb  37890  bj-nfs1t2  37894  bj-hbaeb2  37921  bj-equsal1  37927  bj-equsal2  37928  2stdpc5  37932  bj-ceqsalt0  37987  bj-ceqsalt1  37988  bj-abv  38009  bj-bm1.3ii  38183  bj-axnul  38192  bj-rep  38193  exrecfnlem  38507  wl-dfcleq  38642  wl-moae  38653  wl-aleq  38672  wl-sb8ft  38687  wl-sb8eft  38688  wl-lem-nexmo  38704  wl-axc11rc11  38720  phpreu  38732  findcard4  38837  nninfnub  38888  mpobi123f  39297  eqab2  39385  trcoss  39707  hba1-o  40157  aecom-o  40161  ax12fromc15  40165  hbequid  40169  axc711  40174  axc711toc7  40176  axc711to11  40177  axc5c711  40178  axc5c711toc7  40180  axc5c711to11  40181  equidqe  40182  equid1ALT  40185  axc11nfromc11  40186  axc11n-16  40198  ax12eq  40201  ax12el  40202  ax12indi  40204  eu6w  43891  dfac11  44268  intimag  44859  intimasn  44860  frege70  45136  pm11.12  45562  2albi  45565  2exbi  45567  pm11.57  45576  pm11.61  45580  axc5c4c711toc7  45591  axc5c4c711to11  45592  axc11next  45593  pm13.192  45597  ralbidar  45630  rexbidar  45631  hbntal  45738  hbimpg  45739  hbexg  45741  ax6e2nd  45743  hbimpgVD  46088  ax6e2eqVD  46091  ax6e2ndVD  46092  ax6e2ndALT  46114  ssclaxsep  46178  quantgodelALT  48100  absnsb  48312  rexrsb  48386  ichal  48763