Theorem alimi 1810

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-gen 1794  ax-4 1808

This theorem is referenced by:  2alimi  1811  ala1  1812  sylg  1822  19.38  1838  19.26  1869  19.33  1883  alcomimw  2041  hba1w  2046  hbalw  2048  exexw  2050  naev2  2060  2stdpc4  2069  spsbbi  2072  hbal  2166  hbsbwOLD  2171  nfim1  2198  axc4  2320  axc16i  2440  sb4a  2484  dfmoeu  2535  nexmo  2540  moimi  2544  eu6  2573  darii  2664  cesare  2671  camestres  2672  festino  2673  baroco  2675  darapti  2683  calemes  2686  fesapo  2690  eqeq1d  2738  ralimi2  3077  rgen2a  3370  rmoeq1  3415  ceqsal1t  3513  spcgft  3548  vtoclgft  3551  rspct  3607  elabgt  3671  elabgtOLD  3672  reu6  3731  sbciegftOLD  3825  csbeq2  3903  ssrmof  4050  ralss  4057  rabss2  4077  csbnestgfw  4421  csbnestgf  4426  undif4  4466  ralidmw  4507  ralidm  4511  ralf0  4513  falseral0  4515  intmin4  4976  dfiin2g  5031  invdisj  5128  disjss3  5141  axrep2  5281  sepex  5299  ax6vsep  5302  axnul  5304  csbexg  5309  axpow3  5367  nfnid  5374  axprALT  5421  axprlem1  5422  axprlem4  5425  axprlem4OLD  5428  axprlem5OLD  5429  axprOLD  5430  ssrelrel  5805  iresn0n0  6071  iotanul  6538  iota4  6541  fundif  6614  fv3  6923  zfrep6  7980  ssfi  9214  dfom3  9688  dfac5  10170  dfac2a  10171  dfac2b  10172  kmlem13  10204  zorng  10545  brdom3  10569  brdom4  10571  axpowndlem2  10639  axregnd  10645  axacndlem1  10648  axacndlem2  10649  axacndlem3  10650  axacndlem4  10651  axacnd  10653  ingru  10856  dfnn2  12280  trclfvcotr  15049  prodeq2w  15947  2ndcdisj2  23466  elons2  28282  dfn0s2  28337  pjnormssi  32188  disjin  32600  disjin2  32601  ssdifidlprm  33487  bnj1172  35016  bnj1174  35018  bnj1176  35020  bnj1523  35086  axsepg2  35097  axsepg2ALT  35098  fineqvpow  35111  elpotr  35783  dfon2lem8  35792  distel  35805  hbimtg  35808  bj-gl4  36597  bj-alanim  36614  bj-2albi  36615  bj-exalim  36634  bj-cbvalimt  36641  bj-cbveximt  36642  bj-eximALT  36643  bj-aleximiALT  36644  bj-ssbid2ALT  36665  bj-sb  36689  bj-hbext  36712  bj-nfalt  36713  bj-nfext  36714  bj-nnfalt  36768  bj-nnfext  36769  bj-cbv3tb  36789  bj-nfs1t2  36793  bj-hbaeb2  36820  bj-equsal1  36826  bj-equsal2  36827  2stdpc5  36831  bj-ceqsalt0  36886  bj-ceqsalt1  36887  bj-abv  36908  bj-bm1.3ii  37066  exrecfnlem  37381  wl-moae  37518  wl-aleq  37537  wl-sb8ft  37552  wl-sb8eft  37553  wl-lem-nexmo  37569  wl-axc11rc11  37585  phpreu  37612  nninfnub  37759  mpobi123f  38170  trcoss  38484  hba1-o  38899  aecom-o  38903  ax12fromc15  38907  hbequid  38911  axc711  38916  axc711toc7  38918  axc711to11  38919  axc5c711  38920  axc5c711toc7  38922  axc5c711to11  38923  equidqe  38924  equid1ALT  38927  axc11nfromc11  38928  axc11n-16  38940  ax12eq  38943  ax12el  38944  ax12indi  38946  eu6w  42691  dfac11  43079  intimag  43674  intimasn  43675  frege70  43951  pm11.12  44399  2albi  44402  2exbi  44404  pm11.57  44413  pm11.61  44417  axc5c4c711toc7  44428  axc5c4c711to11  44429  axc11next  44430  pm13.192  44434  ralbidar  44469  rexbidar  44470  hbntal  44578  hbimpg  44579  hbexg  44581  ax6e2nd  44583  hbimpgVD  44929  ax6e2eqVD  44932  ax6e2ndVD  44933  ax6e2ndALT  44955  ssclaxsep  45004  absnsb  47044  rexrsb  47117  ichal  47458  setrec1lem2  49262  setrec1lem4  49264