Theorem alimi 1819

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

Syntax hints:   → wi 4  ∀wal 1541

This theorem was proved from axioms:  ax-mp 5  ax-gen 1803  ax-4 1817

This theorem is referenced by:  2alimi  1820  ala1  1821  sylg  1830  19.38  1846  19.26  1878  19.33  1892  alcomiw  2053  alcomiwOLD  2054  hba1w  2057  hbalw  2059  naev2  2069  2stdpc4  2078  spsbbi  2081  hbal  2173  hbsbw  2175  nfim1  2199  sbequ2OLD  2249  axc4  2322  axc16i  2435  sb4a  2483  dfmoeu  2535  nexmo  2540  moimi  2544  eu6  2573  darii  2665  cesare  2672  camestres  2673  festino  2674  baroco  2676  darapti  2684  calemes  2687  fesapo  2691  eqeq1d  2738  ralimi2  3070  rgen2a  3142  ceqsalt  3428  spcgft  3493  rspct  3513  elabgt  3570  elabgtOLD  3571  reu6  3628  sbciegft  3721  csbeq2  3803  ssrmof  3952  rabss2  3977  csbnestgfw  4320  csbnestgf  4325  undif4  4367  ralidmw  4405  ralidm  4409  ralf0  4411  falseral0  4417  intmin4  4874  dfiin2g  4927  invdisj  5023  disjss3  5038  axrep2  5167  ax6vsep  5181  axnul  5183  csbexg  5188  nfnid  5253  axprALT  5300  axprlem1  5301  axprlem4  5304  axprlem5  5305  axpr  5306  ssrelrel  5651  iresn0n0  5908  iotanul  6336  iota4  6339  fundif  6407  fv3  6713  zfrep6  7706  ssfi  8829  dfom3  9240  dfac5  9707  dfac2a  9708  dfac2b  9709  kmlem13  9741  zorng  10083  brdom3  10107  brdom4  10109  axpowndlem2  10177  axregnd  10183  axacndlem1  10186  axacndlem2  10187  axacndlem3  10188  axacndlem4  10189  axacnd  10191  ingru  10394  dfnn2  11808  trclfvcotr  14537  prodeq2w  15437  2ndcdisj2  22308  pjnormssi  30203  disjin  30598  disjin2  30599  bnj1172  32648  bnj1174  32650  bnj1176  32652  bnj1523  32718  fineqvpow  32732  elpotr  33427  dfon2lem8  33436  distel  33449  hbimtg  33452  bj-gl4  34463  bj-alanim  34480  bj-2albi  34481  bj-exalim  34499  bj-cbvalimt  34506  bj-cbveximt  34507  bj-eximALT  34508  bj-aleximiALT  34509  bj-ssbid2ALT  34530  bj-sb  34555  bj-hbext  34578  bj-nfalt  34579  bj-nfext  34580  bj-nnfalt  34634  bj-nnfext  34635  bj-cbv3tb  34655  bj-nfs1t2  34659  bj-hbaeb2  34687  bj-equsal1  34693  bj-equsal2  34694  2stdpc5  34698  bj-ceqsalt0  34756  bj-ceqsalt1  34757  bj-abv  34778  bj-bm1.3ii  34921  exrecfnlem  35236  wl-moae  35361  wl-aleq  35380  wl-lem-nexmo  35408  wl-axc11rc11  35420  phpreu  35447  nninfnub  35595  mpobi123f  36006  trcoss  36286  hba1-o  36597  aecom-o  36601  ax12fromc15  36605  hbequid  36609  axc711  36614  axc711toc7  36616  axc711to11  36617  axc5c711  36618  axc5c711toc7  36620  axc5c711to11  36621  equidqe  36622  equid1ALT  36625  axc11nfromc11  36626  axc11n-16  36638  ax12eq  36641  ax12el  36642  ax12indi  36644  dfac11  40531  intimag  40882  intimasn  40883  frege70  41159  pm11.12  41607  2albi  41610  2exbi  41612  pm11.57  41621  pm11.61  41625  axc5c4c711toc7  41636  axc5c4c711to11  41637  axc11next  41638  pm13.192  41642  ralbidar  41677  rexbidar  41678  hbntal  41787  hbimpg  41788  hbexg  41790  ax6e2nd  41792  hbimpgVD  42138  ax6e2eqVD  42141  ax6e2ndVD  42142  ax6e2ndALT  42164  absnsb  44136  rexrsb  44207  ichal  44534  setrec1lem2  46008  setrec1lem4  46010