Theorem alimi 1834

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

Syntax hints:   → wi 4  ∀wal 1561

This theorem was proved from axioms:  ax-mp 5  ax-gen 1818  ax-4 1832

This theorem is referenced by:  2alimi  1835  ala1  1836  sylg  1846  19.38  1862  19.26  1893  19.33  1907  alcomimw  2066  hba1w  2072  hbalw  2074  exexw  2076  naev2  2086  2stdpc4  2104  spsbbi  2109  hbal  2204  nfim1  2237  axc4  2356  axc16i  2470  sb4a  2514  dfmoeu  2565  nexmo  2571  eu6  2604  darii  2694  cesare  2701  camestres  2702  festino  2703  baroco  2705  darapti  2713  calemes  2716  fesapo  2720  eqeq1d  2767  ralimi2  3097  rgen2a  3361  rmoeq1  3401  ceqsal1t  3489  spcgft  3520  vtoclgft  3523  rspct  3570  elabgt  3634  elabgtOLD  3635  reu6  3692  csbeq2  3860  ssrmof  4007  ralss  4012  rabss2OLD  4034  csbnestgfw  4379  csbnestgf  4384  undif4  4424  rzal  4451  falseral0OLD  4472  ralidmw  4473  ralidm  4474  intmin4  4938  dfiin2g  4991  invdisj  5091  disjss3  5104  axrep2  5235  replem  5243  zfrep6  5244  sepex  5255  ax6vsep  5258  axnul  5260  csbexg  5265  axpow3  5330  nfnid  5337  axprALT  5384  axprlem1  5385  axprlem4  5388  axprlem1OLD  5390  axprlem4OLD  5392  axprlem5OLD  5393  axprOLD  5394  axprg  5399  ssrelrel  5773  iresn0n0  6047  iotanul  6505  iota4  6506  fundif  6574  fv3  6889  zfrep6OLD  7940  ssfi  9145  elirrvOLD  9548  dfom3  9604  dfac5  10100  dfac2a  10101  dfac2b  10102  kmlem13  10134  zorng  10476  brdom3  10500  brdom4  10502  axpowndlem2  10571  axregnd  10577  axacndlem1  10580  axacndlem2  10581  axacndlem3  10582  axacndlem4  10583  axacnd  10585  ingru  10788  dfnn2  12237  trclfvcotr  15036  prodeq2w  15954  ssdifidlprm  21446  2ndcdisj2  23575  elons2  28409  dfn0s2  28483  pjnormssi  32429  disjin  32841  disjin2  32842  bnj1172  35306  bnj1174  35308  bnj1176  35310  bnj1523  35376  axprALT2  35417  r1omhfb  35420  fineqvpow  35423  r1omhfbregs  35445  axsepg2  35448  axsepg3  35449  axsepg3ALT  35450  axsepg4  35451  axpowg2  35455  axpowg3  35456  elpotr  36142  dfon2lem8  36151  distel  36164  hbimtg  36167  axtco1from2  36848  axtcond  36851  mh-setindnd  36910  bj-gl4  37050  bj-almpi  37074  bj-alanim  37082  bj-2albi  37083  bj-exim  37094  bj-aleximiALT  37096  bj-exalim  37099  bj-cbvaw  37125  bj-cbveaw  37127  bj-ssbid2ALT  37147  bj-sb  37174  bj-nfalt  37200  bj-nfext  37201  bj-nnfbd0  37235  bj-nnfalt  37277  bj-nnfext  37278  bj-cbv3tb  37284  bj-nfs1t2  37288  bj-hbaeb2  37315  bj-equsal1  37321  bj-equsal2  37322  2stdpc5  37326  bj-ceqsalt0  37381  bj-ceqsalt1  37382  bj-abv  37403  bj-bm1.3ii  37561  bj-axnul  37569  bj-rep  37570  exrecfnlem  37885  wl-dfcleq  38020  wl-moae  38031  wl-aleq  38050  wl-sb8ft  38065  wl-sb8eft  38066  wl-lem-nexmo  38082  wl-axc11rc11  38098  phpreu  38115  nninfnub  38262  mpobi123f  38673  eqab2  38761  trcoss  39083  hba1-o  39533  aecom-o  39537  ax12fromc15  39541  hbequid  39545  axc711  39550  axc711toc7  39552  axc711to11  39553  axc5c711  39554  axc5c711toc7  39556  axc5c711to11  39557  equidqe  39558  equid1ALT  39561  axc11nfromc11  39562  axc11n-16  39574  ax12eq  39577  ax12el  39578  ax12indi  39580  eu6w  43270  dfac11  43651  intimag  44244  intimasn  44245  frege70  44521  pm11.12  44949  2albi  44952  2exbi  44954  pm11.57  44963  pm11.61  44967  axc5c4c711toc7  44978  axc5c4c711to11  44979  axc11next  44980  pm13.192  44984  ralbidar  45018  rexbidar  45019  hbntal  45127  hbimpg  45128  hbexg  45130  ax6e2nd  45132  hbimpgVD  45477  ax6e2eqVD  45480  ax6e2ndVD  45481  ax6e2ndALT  45503  ssclaxsep  45556  quantgodelALT  47447  absnsb  47619  rexrsb  47692  ichal  48070  setrec1lem2  50317  setrec1lem4  50319