Theorem alimi 1813

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-gen 1797  ax-4 1811

This theorem is referenced by:  2alimi  1814  ala1  1815  sylg  1825  19.38  1841  19.26  1872  19.33  1886  alcomimw  2045  hba1w  2051  hbalw  2053  exexw  2055  naev2  2065  2stdpc4  2076  spsbbi  2079  hbal  2173  hbsbwOLD  2178  nfim1  2207  axc4  2327  axc16i  2441  sb4a  2485  dfmoeu  2536  nexmo  2542  eu6  2575  darii  2666  cesare  2673  camestres  2674  festino  2675  baroco  2677  darapti  2685  calemes  2688  fesapo  2692  eqeq1d  2739  ralimi2  3070  rgen2a  3334  rmoeq1  3374  ceqsal1t  3463  spcgft  3495  vtoclgft  3498  rspct  3551  elabgt  3615  elabgtOLD  3616  elabgtOLDOLD  3617  reu6  3673  sbciegftOLD  3767  csbeq2  3843  ssrmof  3990  ralss  3997  rabss2OLD  4019  csbnestgfw  4363  csbnestgf  4368  undif4  4408  rzal  4435  falseral0OLD  4456  ralidmw  4457  ralidm  4458  intmin4  4920  dfiin2g  4974  invdisj  5072  disjss3  5085  axrep2  5215  replem  5223  zfrep6  5224  sepex  5235  ax6vsep  5238  axnul  5240  csbexg  5245  axpow3  5305  nfnid  5312  axprALT  5359  axprlem1  5360  axprlem4  5363  axprlem1OLD  5365  axprlem4OLD  5367  axprlem5OLD  5368  axprOLD  5369  axprg  5374  ssrelrel  5745  iresn0n0  6013  iotanul  6472  iota4  6473  fundif  6541  fv3  6852  zfrep6OLD  7901  ssfi  9100  elirrv  9505  dfom3  9559  dfac5  10042  dfac2a  10043  dfac2b  10044  kmlem13  10076  zorng  10417  brdom3  10441  brdom4  10443  axpowndlem2  10512  axregnd  10518  axacndlem1  10521  axacndlem2  10522  axacndlem3  10523  axacndlem4  10524  axacnd  10526  ingru  10729  dfnn2  12178  trclfvcotr  14962  prodeq2w  15866  2ndcdisj2  23432  elons2  28264  dfn0s2  28338  pjnormssi  32254  disjin  32671  disjin2  32672  ssdifidlprm  33533  bnj1172  35159  bnj1174  35161  bnj1176  35163  bnj1523  35229  axsepg2  35241  axsepg2ALT  35242  axprALT2  35269  r1omhfb  35272  fineqvpow  35275  r1omhfbregs  35297  elpotr  35977  dfon2lem8  35986  distel  35999  hbimtg  36002  axtco1from2  36673  axtcond  36676  mh-setindnd  36735  bj-gl4  36876  bj-almpi  36900  bj-alanim  36908  bj-2albi  36909  bj-exim  36920  bj-aleximiALT  36922  bj-exalim  36925  bj-cbvaw  36951  bj-cbveaw  36953  bj-ssbid2ALT  36973  bj-sb  37000  bj-nfalt  37026  bj-nfext  37027  bj-nnfbd0  37061  bj-nnfalt  37103  bj-nnfext  37104  bj-cbv3tb  37110  bj-nfs1t2  37114  bj-hbaeb2  37141  bj-equsal1  37147  bj-equsal2  37148  2stdpc5  37152  bj-ceqsalt0  37207  bj-ceqsalt1  37208  bj-abv  37229  bj-bm1.3ii  37387  bj-axnul  37395  bj-rep  37396  exrecfnlem  37709  wl-dfcleq  37844  wl-moae  37855  wl-aleq  37874  wl-sb8ft  37889  wl-sb8eft  37890  wl-lem-nexmo  37906  wl-axc11rc11  37922  phpreu  37939  nninfnub  38086  mpobi123f  38497  eqab2  38585  trcoss  38907  hba1-o  39357  aecom-o  39361  ax12fromc15  39365  hbequid  39369  axc711  39374  axc711toc7  39376  axc711to11  39377  axc5c711  39378  axc5c711toc7  39380  axc5c711to11  39381  equidqe  39382  equid1ALT  39385  axc11nfromc11  39386  axc11n-16  39398  ax12eq  39401  ax12el  39402  ax12indi  39404  eu6w  43123  dfac11  43508  intimag  44101  intimasn  44102  frege70  44378  pm11.12  44820  2albi  44823  2exbi  44825  pm11.57  44834  pm11.61  44838  axc5c4c711toc7  44849  axc5c4c711to11  44850  axc11next  44851  pm13.192  44855  ralbidar  44889  rexbidar  44890  hbntal  44998  hbimpg  44999  hbexg  45001  ax6e2nd  45003  hbimpgVD  45348  ax6e2eqVD  45351  ax6e2ndVD  45352  ax6e2ndALT  45374  ssclaxsep  45427  absnsb  47487  rexrsb  47560  ichal  47938  setrec1lem2  50175  setrec1lem4  50177