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  2204  axc4  2324  axc16i  2438  sb4a  2482  dfmoeu  2533  nexmo  2538  moimi  2542  eu6  2571  darii  2662  cesare  2669  camestres  2670  festino  2671  baroco  2673  darapti  2681  calemes  2684  fesapo  2688  eqeq1d  2735  ralimi2  3065  rgen2a  3338  rmoeq1  3378  ceqsal1t  3470  spcgft  3503  vtoclgft  3506  rspct  3559  elabgt  3623  elabgtOLD  3624  elabgtOLDOLD  3625  reu6  3681  sbciegftOLD  3775  csbeq2  3851  ssrmof  3998  ralss  4005  rabss2OLD  4027  csbnestgfw  4371  csbnestgf  4376  undif4  4416  ralidmw  4457  ralidm  4461  ralf0  4463  falseral0  4465  intmin4  4927  dfiin2g  4981  invdisj  5079  disjss3  5092  axrep2  5222  sepex  5240  ax6vsep  5243  axnul  5245  csbexg  5250  axpow3  5308  nfnid  5315  axprALT  5362  axprlem1  5363  axprlem4  5366  axprlem4OLD  5369  axprlem5OLD  5370  axprOLD  5371  ssrelrel  5740  iresn0n0  6007  iotanul  6466  iota4  6467  fundif  6535  fv3  6846  zfrep6  7893  ssfi  9089  elirrv  9490  dfom3  9544  dfac5  10027  dfac2a  10028  dfac2b  10029  kmlem13  10061  zorng  10402  brdom3  10426  brdom4  10428  axpowndlem2  10496  axregnd  10502  axacndlem1  10505  axacndlem2  10506  axacndlem3  10507  axacndlem4  10508  axacnd  10510  ingru  10713  dfnn2  12145  trclfvcotr  14918  prodeq2w  15819  2ndcdisj2  23373  elons2  28196  dfn0s2  28261  pjnormssi  32150  disjin  32568  disjin2  32569  ssdifidlprm  33430  bnj1172  35034  bnj1174  35036  bnj1176  35038  bnj1523  35104  axsepg2  35115  axsepg2ALT  35116  r1omhfb  35144  r1omhfbregs  35154  fineqvpow  35159  elpotr  35844  dfon2lem8  35853  distel  35866  hbimtg  35869  bj-gl4  36660  bj-alanim  36677  bj-2albi  36678  bj-exalim  36697  bj-cbvalimt  36704  bj-cbveximt  36705  bj-eximALT  36706  bj-aleximiALT  36707  bj-ssbid2ALT  36728  bj-sb  36752  bj-hbext  36775  bj-nfalt  36776  bj-nfext  36777  bj-nnfalt  36831  bj-nnfext  36832  bj-cbv3tb  36852  bj-nfs1t2  36856  bj-hbaeb2  36883  bj-equsal1  36889  bj-equsal2  36890  2stdpc5  36894  bj-ceqsalt0  36949  bj-ceqsalt1  36950  bj-abv  36971  bj-bm1.3ii  37129  exrecfnlem  37444  wl-moae  37581  wl-aleq  37600  wl-sb8ft  37615  wl-sb8eft  37616  wl-lem-nexmo  37632  wl-axc11rc11  37648  phpreu  37664  nninfnub  37811  mpobi123f  38222  eqab2  38305  trcoss  38604  hba1-o  39016  aecom-o  39020  ax12fromc15  39024  hbequid  39028  axc711  39033  axc711toc7  39035  axc711to11  39036  axc5c711  39037  axc5c711toc7  39039  axc5c711to11  39040  equidqe  39041  equid1ALT  39044  axc11nfromc11  39045  axc11n-16  39057  ax12eq  39060  ax12el  39061  ax12indi  39063  eu6w  42794  dfac11  43179  intimag  43773  intimasn  43774  frege70  44050  pm11.12  44492  2albi  44495  2exbi  44497  pm11.57  44506  pm11.61  44510  axc5c4c711toc7  44521  axc5c4c711to11  44522  axc11next  44523  pm13.192  44527  ralbidar  44561  rexbidar  44562  hbntal  44670  hbimpg  44671  hbexg  44673  ax6e2nd  44675  hbimpgVD  45020  ax6e2eqVD  45023  ax6e2ndVD  45024  ax6e2ndALT  45046  ssclaxsep  45099  absnsb  47151  rexrsb  47224  ichal  47590  setrec1lem2  49813  setrec1lem4  49815