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  2237  axc4  2353  axc16i  2467  sb4a  2511  dfmoeu  2562  nexmo  2568  eu6  2601  darii  2691  cesare  2698  camestres  2699  festino  2700  baroco  2702  darapti  2710  calemes  2713  fesapo  2717  eqeq1d  2764  ralimi2  3096  rgen2a  3358  rmoeq1  3398  ceqsal1t  3485  spcgft  3515  vtoclgft  3518  rspct  3565  elabgt  3629  elabgtOLD  3630  reu6  3687  csbeq2  3855  ssrmof  4002  ralss  4007  rabss2OLD  4029  csbnestgfw  4383  csbnestgf  4388  undif4  4423  rzal  4453  falseral0OLD  4474  ralidmw  4475  ralidm  4476  intmin4  4940  dfiin2g  4993  invdisj  5093  disjss3  5106  axrep2  5239  replem  5247  zfrep6  5248  sepex  5261  ax6vsep  5264  axnul  5266  csbexg  5271  axpow3  5337  nfnid  5344  axprALT  5391  axprlem1  5392  axprlem4  5395  axprlem1OLD  5397  axprlem4OLD  5399  axprlem5OLD  5400  axprOLD  5401  axprg  5406  ssrelrel  5780  iresn0n0  6054  iotanul  6517  iota4  6518  fundif  6586  fv3  6900  zfrep6OLD  7956  ssfi  9171  elirrvOLD  9574  dfom3  9630  dfac5  10135  dfac2a  10136  dfac2b  10137  kmlem13  10169  zorng  10510  brdom3  10535  brdom4  10537  axpowndlem2  10611  axregnd  10617  axacndlem1  10620  axacndlem2  10621  axacndlem3  10622  axacndlem4  10623  axacnd  10625  ingru  10828  dfnn2  12274  trclfvcotr  15086  prodeq2w  16003  ssdifidlprm  21555  2ndcdisj2  23689  elons2  28531  dfn0s2  28605  pjnormssi  32657  disjin  33067  disjin2  33068  bnj1172  35518  bnj1174  35520  bnj1176  35522  bnj1523  35588  axprALT2  35625  r1omhfb  35630  fineqvpow  35649  r1omhfbregs  35671  axsepg2  35674  axsepg3  35675  axsepg3ALT  35676  axsepg4  35677  axpowg2  35681  axpowg3  35682  elpotr  36366  dfon2lem8  36375  distel  36388  hbimtg  36391  axtco1from2  37102  axtcond  37105  mh-setindnd  37164  bj-gl4  37304  bj-almpi  37328  bj-alanim  37336  bj-2albi  37337  bj-exim  37348  bj-aleximiALT  37350  bj-exalim  37353  bj-cbvaw  37379  bj-cbveaw  37381  bj-ssbid2ALT  37401  bj-sb  37428  bj-nfalt  37454  bj-nfext  37455  bj-nnfbd0  37489  bj-nnfalt  37531  bj-nnfext  37532  bj-cbv3tb  37538  bj-nfs1t2  37542  bj-hbaeb2  37569  bj-equsal1  37575  bj-equsal2  37576  2stdpc5  37580  bj-ceqsalt0  37635  bj-ceqsalt1  37636  bj-abv  37657  bj-bm1.3ii  37816  bj-axnul  37825  bj-rep  37826  exrecfnlem  38141  wl-dfcleq  38276  wl-moae  38287  wl-aleq  38306  wl-sb8ft  38321  wl-sb8eft  38322  wl-lem-nexmo  38338  wl-axc11rc11  38354  phpreu  38366  findcard4  38471  nninfnub  38509  mpobi123f  38918  eqab2  39006  trcoss  39328  hba1-o  39778  aecom-o  39782  ax12fromc15  39786  hbequid  39790  axc711  39795  axc711toc7  39797  axc711to11  39798  axc5c711  39799  axc5c711toc7  39801  axc5c711to11  39802  equidqe  39803  equid1ALT  39806  axc11nfromc11  39807  axc11n-16  39819  ax12eq  39822  ax12el  39823  ax12indi  39825  eu6w  43530  dfac11  43911  intimag  44504  intimasn  44505  frege70  44781  pm11.12  45207  2albi  45210  2exbi  45212  pm11.57  45221  pm11.61  45225  axc5c4c711toc7  45236  axc5c4c711to11  45237  axc11next  45238  pm13.192  45242  ralbidar  45276  rexbidar  45277  hbntal  45384  hbimpg  45385  hbexg  45387  ax6e2nd  45389  hbimpgVD  45734  ax6e2eqVD  45737  ax6e2ndVD  45738  ax6e2ndALT  45760  ssclaxsep  45813  quantgodelALT  47711  absnsb  47923  rexrsb  47996  ichal  48374  setrec1lem2  50622  setrec1lem4  50624