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  2205  nfim1  2238  axc4  2357  axc16i  2471  sb4a  2515  dfmoeu  2566  nexmo  2572  eu6  2605  darii  2695  cesare  2702  camestres  2703  festino  2704  baroco  2706  darapti  2714  calemes  2717  fesapo  2721  eqeq1d  2768  ralimi2  3100  rgen2a  3363  rmoeq1  3403  ceqsal1t  3490  spcgft  3520  vtoclgft  3523  rspct  3570  elabgt  3634  elabgtOLD  3635  reu6  3692  csbeq2  3861  ssrmof  4008  ralss  4013  rabss2OLD  4035  csbnestgfw  4390  csbnestgf  4395  undif4  4430  rzal  4460  falseral0OLD  4481  ralidmw  4482  ralidm  4483  intmin4  4947  dfiin2g  5000  invdisj  5100  disjss3  5113  axrep2  5246  replem  5254  zfrep6  5255  sepex  5268  ax6vsep  5271  axnul  5273  csbexg  5278  axpow3  5344  nfnid  5351  axprALT  5398  axprlem1  5399  axprlem4  5402  axprlem1OLD  5404  axprlem4OLD  5406  axprlem5OLD  5407  axprOLD  5408  axprg  5413  ssrelrel  5787  iresn0n0  6061  iotanul  6523  iota4  6524  fundif  6592  fv3  6906  zfrep6OLD  7961  ssfi  9167  elirrvOLD  9570  dfom3  9626  dfac5  10131  dfac2a  10132  dfac2b  10133  kmlem13  10165  zorng  10506  brdom3  10530  brdom4  10532  axpowndlem2  10601  axregnd  10607  axacndlem1  10610  axacndlem2  10611  axacndlem3  10612  axacndlem4  10613  axacnd  10615  ingru  10818  dfnn2  12264  trclfvcotr  15072  prodeq2w  15990  ssdifidlprm  21523  2ndcdisj2  23651  elons2  28488  dfn0s2  28562  pjnormssi  32557  disjin  32968  disjin2  32969  bnj1172  35421  bnj1174  35423  bnj1176  35425  bnj1523  35491  axprALT2  35528  r1omhfb  35533  fineqvpow  35552  r1omhfbregs  35574  axsepg2  35577  axsepg3  35578  axsepg3ALT  35579  axsepg4  35580  axpowg2  35584  axpowg3  35585  elpotr  36292  dfon2lem8  36301  distel  36314  hbimtg  36317  axtco1from2  37027  axtcond  37030  mh-setindnd  37089  bj-gl4  37229  bj-almpi  37253  bj-alanim  37261  bj-2albi  37262  bj-exim  37273  bj-aleximiALT  37275  bj-exalim  37278  bj-cbvaw  37304  bj-cbveaw  37306  bj-ssbid2ALT  37326  bj-sb  37353  bj-nfalt  37379  bj-nfext  37380  bj-nnfbd0  37414  bj-nnfalt  37456  bj-nnfext  37457  bj-cbv3tb  37463  bj-nfs1t2  37467  bj-hbaeb2  37494  bj-equsal1  37500  bj-equsal2  37501  2stdpc5  37505  bj-ceqsalt0  37560  bj-ceqsalt1  37561  bj-abv  37582  bj-bm1.3ii  37741  bj-axnul  37750  bj-rep  37751  exrecfnlem  38066  wl-dfcleq  38201  wl-moae  38212  wl-aleq  38231  wl-sb8ft  38246  wl-sb8eft  38247  wl-lem-nexmo  38263  wl-axc11rc11  38279  phpreu  38296  nninfnub  38443  mpobi123f  38852  eqab2  38940  trcoss  39262  hba1-o  39712  aecom-o  39716  ax12fromc15  39720  hbequid  39724  axc711  39729  axc711toc7  39731  axc711to11  39732  axc5c711  39733  axc5c711toc7  39735  axc5c711to11  39736  equidqe  39737  equid1ALT  39740  axc11nfromc11  39741  axc11n-16  39753  ax12eq  39756  ax12el  39757  ax12indi  39759  eu6w  43449  dfac11  43830  intimag  44423  intimasn  44424  frege70  44700  pm11.12  45126  2albi  45129  2exbi  45131  pm11.57  45140  pm11.61  45144  axc5c4c711toc7  45155  axc5c4c711to11  45156  axc11next  45157  pm13.192  45161  ralbidar  45195  rexbidar  45196  hbntal  45303  hbimpg  45304  hbexg  45306  ax6e2nd  45308  hbimpgVD  45653  ax6e2eqVD  45656  ax6e2ndVD  45657  ax6e2ndALT  45679  ssclaxsep  45732  quantgodelALT  47630  absnsb  47805  rexrsb  47878  ichal  48256  setrec1lem2  50507  setrec1lem4  50509