Theorem alimi 1808

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-gen 1792  ax-4 1806

This theorem is referenced by:  2alimi  1809  ala1  1810  sylg  1820  19.38  1836  19.26  1868  19.33  1882  alcomimw  2040  hba1w  2045  hbalw  2047  exexw  2049  naev2  2059  2stdpc4  2068  spsbbi  2071  hbal  2165  hbsbwOLD  2170  nfim1  2197  axc4  2320  axc16i  2439  sb4a  2483  dfmoeu  2534  nexmo  2539  moimi  2543  eu6  2572  darii  2663  cesare  2670  camestres  2671  festino  2672  baroco  2674  darapti  2682  calemes  2685  fesapo  2689  eqeq1d  2737  ralimi2  3076  rgen2a  3369  rmoeq1  3414  ceqsal1t  3512  spcgft  3549  vtoclgft  3552  rspct  3608  elabgt  3672  elabgtOLD  3673  elabgtOLDOLD  3674  reu6  3735  sbciegftOLD  3830  csbeq2  3913  ssrmof  4063  rabss2  4088  csbnestgfw  4428  csbnestgf  4433  undif4  4473  ralidmw  4514  ralidm  4518  ralf0  4520  falseral0  4522  intmin4  4982  dfiin2g  5037  invdisj  5134  disjss3  5147  axrep2  5288  sepex  5306  ax6vsep  5309  axnul  5311  csbexg  5316  nfnid  5381  axprALT  5428  axprlem1  5429  axprlem4  5432  axprlem4OLD  5435  axprlem5OLD  5436  axprOLD  5437  ssrelrel  5809  iresn0n0  6074  iotanul  6541  iota4  6544  fundif  6617  fv3  6925  zfrep6  7978  ssfi  9212  dfom3  9685  dfac5  10167  dfac2a  10168  dfac2b  10169  kmlem13  10201  zorng  10542  brdom3  10566  brdom4  10568  axpowndlem2  10636  axregnd  10642  axacndlem1  10645  axacndlem2  10646  axacndlem3  10647  axacndlem4  10648  axacnd  10650  ingru  10853  dfnn2  12277  trclfvcotr  15045  prodeq2w  15943  2ndcdisj2  23481  elons2  28296  dfn0s2  28351  pjnormssi  32197  disjin  32606  disjin2  32607  ssdifidlprm  33466  bnj1172  34994  bnj1174  34996  bnj1176  34998  bnj1523  35064  axsepg2  35075  axsepg2ALT  35076  fineqvpow  35089  elpotr  35763  dfon2lem8  35772  distel  35785  hbimtg  35788  bj-gl4  36578  bj-alanim  36595  bj-2albi  36596  bj-exalim  36615  bj-cbvalimt  36622  bj-cbveximt  36623  bj-eximALT  36624  bj-aleximiALT  36625  bj-ssbid2ALT  36646  bj-sb  36670  bj-hbext  36693  bj-nfalt  36694  bj-nfext  36695  bj-nnfalt  36749  bj-nnfext  36750  bj-cbv3tb  36770  bj-nfs1t2  36774  bj-hbaeb2  36801  bj-equsal1  36807  bj-equsal2  36808  2stdpc5  36812  bj-ceqsalt0  36867  bj-ceqsalt1  36868  bj-abv  36889  bj-bm1.3ii  37047  exrecfnlem  37362  wl-moae  37497  wl-aleq  37516  wl-sb8ft  37531  wl-sb8eft  37532  wl-lem-nexmo  37548  wl-axc11rc11  37564  phpreu  37591  nninfnub  37738  mpobi123f  38149  trcoss  38464  hba1-o  38879  aecom-o  38883  ax12fromc15  38887  hbequid  38891  axc711  38896  axc711toc7  38898  axc711to11  38899  axc5c711  38900  axc5c711toc7  38902  axc5c711to11  38903  equidqe  38904  equid1ALT  38907  axc11nfromc11  38908  axc11n-16  38920  ax12eq  38923  ax12el  38924  ax12indi  38926  eu6w  42663  dfac11  43051  intimag  43646  intimasn  43647  frege70  43923  pm11.12  44371  2albi  44374  2exbi  44376  pm11.57  44385  pm11.61  44389  axc5c4c711toc7  44400  axc5c4c711to11  44401  axc11next  44402  pm13.192  44406  ralbidar  44441  rexbidar  44442  hbntal  44551  hbimpg  44552  hbexg  44554  ax6e2nd  44556  hbimpgVD  44902  ax6e2eqVD  44905  ax6e2ndVD  44906  ax6e2ndALT  44928  ssclaxsep  44947  absnsb  46977  rexrsb  47050  ichal  47391  setrec1lem2  48919  setrec1lem4  48921