Theorem alimi 1843

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-gen 1827  ax-4 1841

This theorem is used by:  2alimi  1844  ala1  1845  sylg  1855  19.38  1871  19.26  1902  19.33  1916  alcomimw  2075  hba1w  2081  hbalw  2083  exexw  2085  naev2  2095  2stdpc4  2106  spsbbi  2109  hbal  2203  nfim1  2235  axc4  2351  axc16i  2465  sb4a  2509  dfmoeu  2560  nexmo  2566  eu6  2599  darii  2689  cesare  2696  camestres  2697  festino  2698  baroco  2700  darapti  2708  calemes  2711  fesapo  2715  eqeq1d  2762  ralimi2  3094  rgen2a  3356  rmoeq1  3396  ceqsal1t  3482  spcgft  3512  vtoclgft  3515  rspct  3562  elabgt  3625  elabgtOLD  3626  reu6  3683  csbeq2  3851  ssrmof  3976  ralss  3981  rabss2OLD  4003  csbnestgfw  4379  csbnestgf  4384  undif4  4419  rzal  4449  falseral0OLD  4470  ralidmw  4471  ralidm  4472  intmin4  4936  dfiin2g  4988  invdisj  5088  disjss3  5101  axrep2  5234  replem  5240  zfrep6  5241  sepex  5254  ax6vsep  5256  axnul  5258  csbexg  5263  axpow3  5329  nfnid  5336  axprALT  5383  axprlem1  5384  axprlem4  5387  axprlem1OLD  5389  axprg  5394  ssrelrel  5771  iresn0n0  6045  iotanul  6518  iota4  6519  fundif  6589  fv3  6903  zfrep6OLD  7967  ssfi  9191  elirrvOLD  9595  dfom3  9651  setrec1lem2  9970  setrec1lem4  9974  dfac5  10210  dfac2a  10211  dfac2b  10212  kmlem13  10244  zorng  10585  brdom3  10610  brdom4  10612  axpowndlem2  10686  axregnd  10692  axacndlem1  10695  axacndlem2  10696  axacndlem3  10697  axacndlem4  10698  axacnd  10700  ingru  10903  dfnn2  12351  trclfvcotr  15167  prodeq2w  16084  ssdifidlprm  21647  2ndcdisj2  23781  elons2  28649  dfn0s2  28723  pjnormssi  32775  disjin  33227  disjin2  33228  bnj1172  35677  bnj1174  35679  bnj1176  35681  bnj1523  35747  reu6f  35755  rmo6  35756  axprALT2  35786  r1omhfb  35790  dfac15  35809  dfac16  35810  fineqvpow  35839  r1omhfbregs  35861  axsepg2  35864  axsepg3  35865  axsepg3ALT  35866  axsepg4  35867  axpowg2  35871  axpowg3  35872  onprcf1acwevdlem2  35965  elpotr  36635  dfon2lem8  36644  distel  36657  hbimtg  36660  axtco1from2  37355  axtcond  37358  mh-setindnd  37417  bj-gl4  37557  bj-almpi  37581  bj-alanim  37589  bj-2albi  37590  bj-exim  37601  bj-aleximiALT  37603  bj-exalim  37606  bj-cbvaw  37632  bj-cbveaw  37634  bj-ssbid2ALT  37654  bj-sb  37681  bj-nfalt  37707  bj-nfext  37708  bj-nnfbd0  37742  bj-nnfalt  37784  bj-nnfext  37785  bj-cbv3tb  37791  bj-nfs1t2  37795  bj-hbaeb2  37822  bj-equsal1  37828  bj-equsal2  37829  2stdpc5  37833  bj-ceqsalt0  37888  bj-ceqsalt1  37889  bj-abv  37910  bj-bm1.3ii  38071  bj-axnul  38080  bj-rep  38081  exrecfnlem  38395  wl-dfcleq  38530  wl-moae  38541  wl-aleq  38560  wl-sb8ft  38575  wl-sb8eft  38576  wl-lem-nexmo  38592  wl-axc11rc11  38608  phpreu  38620  findcard4  38725  nninfnub  38778  mpobi123f  39187  eqab2  39275  trcoss  39597  hba1-o  40047  aecom-o  40051  ax12fromc15  40055  hbequid  40059  axc711  40064  axc711toc7  40066  axc711to11  40067  axc5c711  40068  axc5c711toc7  40070  axc5c711to11  40071  equidqe  40072  equid1ALT  40075  axc11nfromc11  40076  axc11n-16  40088  ax12eq  40091  ax12el  40092  ax12indi  40094  eu6w  43780  dfac11  44157  intimag  44749  intimasn  44750  frege70  45026  pm11.12  45452  2albi  45455  2exbi  45457  pm11.57  45466  pm11.61  45470  axc5c4c711toc7  45481  axc5c4c711to11  45482  axc11next  45483  pm13.192  45487  ralbidar  45521  rexbidar  45522  hbntal  45629  hbimpg  45630  hbexg  45632  ax6e2nd  45634  hbimpgVD  45979  ax6e2eqVD  45982  ax6e2ndVD  45983  ax6e2ndALT  46005  ssclaxsep  46065  quantgodelALT  47978  absnsb  48190  rexrsb  48263  ichal  48641