Theorem alimi 1812

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-gen 1796  ax-4 1810

This theorem is referenced by:  2alimi  1813  ala1  1814  sylg  1824  19.38  1840  19.26  1871  19.33  1885  alcomimw  2044  hba1w  2050  hbalw  2052  exexw  2054  naev2  2064  2stdpc4  2075  spsbbi  2078  hbal  2172  hbsbwOLD  2177  nfim1  2206  axc4  2326  axc16i  2440  sb4a  2484  dfmoeu  2535  nexmo  2541  eu6  2574  darii  2665  cesare  2672  camestres  2673  festino  2674  baroco  2676  darapti  2684  calemes  2687  fesapo  2691  eqeq1d  2738  ralimi2  3068  rgen2a  3341  rmoeq1  3381  ceqsal1t  3473  spcgft  3506  vtoclgft  3509  rspct  3562  elabgt  3626  elabgtOLD  3627  elabgtOLDOLD  3628  reu6  3684  sbciegftOLD  3778  csbeq2  3854  ssrmof  4001  ralss  4008  rabss2OLD  4030  csbnestgfw  4374  csbnestgf  4379  undif4  4419  rzal  4447  falseral0OLD  4468  ralidmw  4469  ralidm  4470  intmin4  4932  dfiin2g  4986  invdisj  5084  disjss3  5097  axrep2  5227  sepex  5245  ax6vsep  5248  axnul  5250  csbexg  5255  axpow3  5313  nfnid  5320  axprALT  5367  axprlem1  5368  axprlem4  5371  axprlem4OLD  5374  axprlem5OLD  5375  axprOLD  5376  ssrelrel  5745  iresn0n0  6013  iotanul  6472  iota4  6473  fundif  6541  fv3  6852  zfrep6  7899  ssfi  9097  elirrv  9502  dfom3  9556  dfac5  10039  dfac2a  10040  dfac2b  10041  kmlem13  10073  zorng  10414  brdom3  10438  brdom4  10440  axpowndlem2  10509  axregnd  10515  axacndlem1  10518  axacndlem2  10519  axacndlem3  10520  axacndlem4  10521  axacnd  10523  ingru  10726  dfnn2  12158  trclfvcotr  14932  prodeq2w  15833  2ndcdisj2  23401  elons2  28254  dfn0s2  28328  pjnormssi  32243  disjin  32661  disjin2  32662  ssdifidlprm  33539  bnj1172  35157  bnj1174  35159  bnj1176  35161  bnj1523  35227  axsepg2  35238  axsepg2ALT  35239  r1omhfb  35268  fineqvpow  35271  r1omhfbregs  35293  elpotr  35973  dfon2lem8  35982  distel  35995  hbimtg  35998  mh-setindnd  36667  bj-gl4  36795  bj-alanim  36812  bj-2albi  36813  bj-exalim  36832  bj-cbvalimt  36839  bj-cbveximt  36840  bj-eximALT  36841  bj-aleximiALT  36842  bj-ssbid2ALT  36864  bj-sb  36888  bj-hbext  36911  bj-nfalt  36912  bj-nfext  36913  bj-nnfalt  36967  bj-nnfext  36968  bj-cbv3tb  36988  bj-nfs1t2  36992  bj-hbaeb2  37019  bj-equsal1  37025  bj-equsal2  37026  2stdpc5  37030  bj-ceqsalt0  37085  bj-ceqsalt1  37086  bj-abv  37107  bj-bm1.3ii  37265  exrecfnlem  37580  wl-moae  37717  wl-aleq  37736  wl-sb8ft  37751  wl-sb8eft  37752  wl-lem-nexmo  37768  wl-axc11rc11  37784  phpreu  37801  nninfnub  37948  mpobi123f  38359  eqab2  38442  trcoss  38741  hba1-o  39153  aecom-o  39157  ax12fromc15  39161  hbequid  39165  axc711  39170  axc711toc7  39172  axc711to11  39173  axc5c711  39174  axc5c711toc7  39176  axc5c711to11  39177  equidqe  39178  equid1ALT  39181  axc11nfromc11  39182  axc11n-16  39194  ax12eq  39197  ax12el  39198  ax12indi  39200  eu6w  42915  dfac11  43300  intimag  43893  intimasn  43894  frege70  44170  pm11.12  44612  2albi  44615  2exbi  44617  pm11.57  44626  pm11.61  44630  axc5c4c711toc7  44641  axc5c4c711to11  44642  axc11next  44643  pm13.192  44647  ralbidar  44681  rexbidar  44682  hbntal  44790  hbimpg  44791  hbexg  44793  ax6e2nd  44795  hbimpgVD  45140  ax6e2eqVD  45143  ax6e2ndVD  45144  ax6e2ndALT  45166  ssclaxsep  45219  absnsb  47269  rexrsb  47342  ichal  47708  setrec1lem2  49929  setrec1lem4  49931