Theorem alimi 1809

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-gen 1793  ax-4 1807

This theorem is referenced by:  2alimi  1810  ala1  1811  sylg  1821  19.38  1837  19.26  1869  19.33  1883  alcomimw  2042  hba1w  2047  hbalw  2049  exexw  2051  naev2  2061  2stdpc4  2070  spsbbi  2073  hbal  2168  hbsbwOLD  2173  nfim1  2200  axc4  2325  axc16i  2444  sb4a  2488  dfmoeu  2539  nexmo  2544  moimi  2548  eu6  2577  darii  2668  cesare  2675  camestres  2676  festino  2677  baroco  2679  darapti  2687  calemes  2690  fesapo  2694  eqeq1d  2742  ralimi2  3084  rgen2a  3379  rmoeq1  3425  ceqsal1t  3522  spcgft  3561  vtoclgft  3564  rspct  3621  elabgt  3685  elabgtOLD  3686  elabgtOLDOLD  3687  reu6  3748  sbciegftOLD  3843  csbeq2  3926  ssrmof  4076  rabss2  4101  csbnestgfw  4445  csbnestgf  4450  undif4  4490  ralidmw  4531  ralidm  4535  ralf0  4537  falseral0  4539  intmin4  5001  dfiin2g  5055  invdisj  5152  disjss3  5165  axrep2  5306  ax6vsep  5321  axnul  5323  csbexg  5328  nfnid  5393  axprALT  5440  axprlem1  5441  axprlem4  5444  axprlem5  5445  axpr  5446  ssrelrel  5820  iresn0n0  6083  iotanul  6551  iota4  6554  fundif  6627  fv3  6938  zfrep6  7995  ssfi  9240  dfom3  9716  dfac5  10198  dfac2a  10199  dfac2b  10200  kmlem13  10232  zorng  10573  brdom3  10597  brdom4  10599  axpowndlem2  10667  axregnd  10673  axacndlem1  10676  axacndlem2  10677  axacndlem3  10678  axacndlem4  10679  axacnd  10681  ingru  10884  dfnn2  12306  trclfvcotr  15058  prodeq2w  15958  2ndcdisj2  23486  elons2  28299  dfn0s2  28354  pjnormssi  32200  disjin  32608  disjin2  32609  ssdifidlprm  33451  bnj1172  34977  bnj1174  34979  bnj1176  34981  bnj1523  35047  axsepg2  35058  axsepg2ALT  35059  fineqvpow  35072  elpotr  35745  dfon2lem8  35754  distel  35767  hbimtg  35770  bj-gl4  36561  bj-alanim  36578  bj-2albi  36579  bj-exalim  36598  bj-cbvalimt  36605  bj-cbveximt  36606  bj-eximALT  36607  bj-aleximiALT  36608  bj-ssbid2ALT  36629  bj-sb  36653  bj-hbext  36676  bj-nfalt  36677  bj-nfext  36678  bj-nnfalt  36732  bj-nnfext  36733  bj-cbv3tb  36753  bj-nfs1t2  36757  bj-hbaeb2  36784  bj-equsal1  36790  bj-equsal2  36791  2stdpc5  36795  bj-ceqsalt0  36850  bj-ceqsalt1  36851  bj-abv  36872  bj-bm1.3ii  37030  exrecfnlem  37345  wl-moae  37470  wl-aleq  37489  wl-sb8ft  37504  wl-sb8eft  37505  wl-lem-nexmo  37521  wl-axc11rc11  37537  phpreu  37564  nninfnub  37711  mpobi123f  38122  trcoss  38438  hba1-o  38853  aecom-o  38857  ax12fromc15  38861  hbequid  38865  axc711  38870  axc711toc7  38872  axc711to11  38873  axc5c711  38874  axc5c711toc7  38876  axc5c711to11  38877  equidqe  38878  equid1ALT  38881  axc11nfromc11  38882  axc11n-16  38894  ax12eq  38897  ax12el  38898  ax12indi  38900  eu6w  42631  dfac11  43019  intimag  43618  intimasn  43619  frege70  43895  pm11.12  44344  2albi  44347  2exbi  44349  pm11.57  44358  pm11.61  44362  axc5c4c711toc7  44373  axc5c4c711to11  44374  axc11next  44375  pm13.192  44379  ralbidar  44414  rexbidar  44415  hbntal  44524  hbimpg  44525  hbexg  44527  ax6e2nd  44529  hbimpgVD  44875  ax6e2eqVD  44878  ax6e2ndVD  44879  ax6e2ndALT  44901  absnsb  46942  rexrsb  47015  ichal  47340  setrec1lem2  48780  setrec1lem4  48782