Theorem alimi 1814

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-gen 1798  ax-4 1812

This theorem is referenced by:  2alimi  1815  ala1  1816  sylg  1825  19.38  1841  19.26  1873  19.33  1887  alcomiw  2046  alcomiwOLD  2047  hba1w  2050  hbalw  2052  exexw  2054  naev2  2064  2stdpc4  2073  spsbbi  2076  hbal  2167  hbsbw  2169  nfim1  2192  sbequ2OLD  2242  axc4  2315  axc16i  2436  sb4a  2484  dfmoeu  2536  nexmo  2541  moimi  2545  eu6  2574  darii  2666  cesare  2673  camestres  2674  festino  2675  baroco  2677  darapti  2685  calemes  2688  fesapo  2692  eqeq1d  2740  ralimi2  3084  rgen2a  3158  ceqsalt  3462  spcgft  3527  rspct  3547  elabgt  3603  elabgtOLD  3604  reu6  3661  sbciegft  3754  csbeq2  3837  ssrmof  3986  rabss2  4011  csbnestgfw  4353  csbnestgf  4358  undif4  4400  ralidmw  4438  ralidm  4442  ralf0  4444  falseral0  4450  intmin4  4908  dfiin2g  4962  invdisj  5058  disjss3  5073  axrep2  5212  ax6vsep  5227  axnul  5229  csbexg  5234  nfnid  5298  axprALT  5345  axprlem1  5346  axprlem4  5349  axprlem5  5350  axpr  5351  ssrelrel  5706  iresn0n0  5963  iotanul  6411  iota4  6414  fundif  6483  fv3  6792  zfrep6  7797  ssfi  8956  dfom3  9405  dfac5  9884  dfac2a  9885  dfac2b  9886  kmlem13  9918  zorng  10260  brdom3  10284  brdom4  10286  axpowndlem2  10354  axregnd  10360  axacndlem1  10363  axacndlem2  10364  axacndlem3  10365  axacndlem4  10366  axacnd  10368  ingru  10571  dfnn2  11986  trclfvcotr  14720  prodeq2w  15622  2ndcdisj2  22608  pjnormssi  30530  disjin  30925  disjin2  30926  bnj1172  32981  bnj1174  32983  bnj1176  32985  bnj1523  33051  fineqvpow  33065  elpotr  33757  dfon2lem8  33766  distel  33779  hbimtg  33782  bj-gl4  34777  bj-alanim  34794  bj-2albi  34795  bj-exalim  34813  bj-cbvalimt  34820  bj-cbveximt  34821  bj-eximALT  34822  bj-aleximiALT  34823  bj-ssbid2ALT  34844  bj-sb  34869  bj-hbext  34892  bj-nfalt  34893  bj-nfext  34894  bj-nnfalt  34948  bj-nnfext  34949  bj-cbv3tb  34969  bj-nfs1t2  34973  bj-hbaeb2  35001  bj-equsal1  35007  bj-equsal2  35008  2stdpc5  35012  bj-ceqsalt0  35069  bj-ceqsalt1  35070  bj-abv  35091  bj-bm1.3ii  35235  exrecfnlem  35550  wl-moae  35675  wl-aleq  35694  wl-lem-nexmo  35722  wl-axc11rc11  35734  phpreu  35761  nninfnub  35909  mpobi123f  36320  trcoss  36600  hba1-o  36911  aecom-o  36915  ax12fromc15  36919  hbequid  36923  axc711  36928  axc711toc7  36930  axc711to11  36931  axc5c711  36932  axc5c711toc7  36934  axc5c711to11  36935  equidqe  36936  equid1ALT  36939  axc11nfromc11  36940  axc11n-16  36952  ax12eq  36955  ax12el  36956  ax12indi  36958  dfac11  40887  intimag  41264  intimasn  41265  frege70  41541  pm11.12  41993  2albi  41996  2exbi  41998  pm11.57  42007  pm11.61  42011  axc5c4c711toc7  42022  axc5c4c711to11  42023  axc11next  42024  pm13.192  42028  ralbidar  42063  rexbidar  42064  hbntal  42173  hbimpg  42174  hbexg  42176  ax6e2nd  42178  hbimpgVD  42524  ax6e2eqVD  42527  ax6e2ndVD  42528  ax6e2ndALT  42550  absnsb  44521  rexrsb  44592  ichal  44918  setrec1lem2  46394  setrec1lem4  46396