Theorem alimi 1793

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

Syntax hints:   → wi 4  ∀wal 1520

This theorem was proved from axioms:  ax-mp 5  ax-gen 1777  ax-4 1791

This theorem is referenced by:  2alimi  1794  ala1  1795  sylg  1804  19.38  1820  19.26  1852  19.33  1866  alcomiw  2022  hba1w  2025  hbalw  2027  hbnaevg  2037  2stdpc4  2048  spsbbi  2051  hbal  2138  nfim1  2164  sbequ2  2214  axc4  2303  axc16i  2415  sb4a  2463  dfmoeu  2572  nexmo  2577  moimi  2581  mobiOLD  2585  eu6  2617  darii  2724  cesare  2731  camestres  2732  festino  2733  baroco  2735  darapti  2743  calemes  2746  fesapo  2750  eqeq1d  2797  ralimi2  3124  rgen2a  3193  ceqsalt  3470  spcgft  3530  rspct  3551  elabgt  3601  reu6  3651  sbciegft  3737  csbeq2  3816  ssrmof  3953  rabss2  3975  csbnestgf  4291  undif4  4330  falseral0  4373  intmin4  4811  dfiin2g  4860  invdisj  4948  disjss3  4961  axrep2  5084  ax6vsep  5098  axnul  5100  csbexg  5105  nfnid  5167  axprALT  5214  axprlem1  5215  axprlem4  5218  axprlem5  5219  axpr  5220  ssrelrel  5555  iotanul  6204  iota4  6207  fundif  6273  fv3  6556  zfrep6  7512  dfom3  8956  dfac5  9400  dfac2a  9401  dfac2b  9402  kmlem13  9434  zorng  9772  brdom3  9796  brdom4  9798  axpowndlem2  9866  axregnd  9872  axacndlem1  9875  axacndlem2  9876  axacndlem3  9877  axacndlem4  9878  axacnd  9880  ingru  10083  dfnn2  11499  trclfvcotr  14203  prodeq2w  15099  2ndcdisj2  21749  pjnormssi  29636  disjin  30026  disjin2  30027  bnj1172  31887  bnj1174  31889  bnj1176  31891  bnj1523  31957  elpotr  32634  dfon2lem8  32643  distel  32657  hbimtg  32660  bj-gl4lem  33534  bj-alanim  33552  bj-2albi  33553  bj-2exbi  33555  bj-exalim  33567  bj-cbvalimt  33574  bj-cbveximt  33575  bj-ssbid2ALT  33595  bj-sb  33620  bj-hbext  33643  bj-nfalt  33644  bj-nfext  33645  bj-cbv3tb  33653  bj-nfs1t2  33657  bj-hbaeb2  33711  bj-equsal1  33717  bj-equsal2  33718  2stdpc5  33722  bj-ceqsalt0  33772  bj-ceqsalt1  33773  bj-nnfalt  33877  bj-nnfext  33878  bj-bm1.3ii  33955  exrecfnlem  34191  wl-moae  34287  wl-aleq  34307  wl-lem-nexmo  34334  wl-axc11rc11  34346  phpreu  34407  nninfnub  34558  mpobi123f  34972  trcoss  35253  hba1-o  35564  aecom-o  35568  ax12fromc15  35572  hbequid  35576  axc711  35581  axc711toc7  35583  axc711to11  35584  axc5c711  35585  axc5c711toc7  35587  axc5c711to11  35588  equidqe  35589  equid1ALT  35592  axc11nfromc11  35593  axc11n-16  35605  ax12eq  35608  ax12el  35609  ax12indi  35611  dfac11  39147  intimag  39486  intimasn  39487  frege70  39764  pm11.12  40245  2albi  40248  2exbi  40250  pm11.57  40259  pm11.61  40263  axc5c4c711toc7  40274  axc5c4c711to11  40275  axc11next  40276  pm13.192  40280  ralbidar  40316  rexbidar  40317  hbntal  40426  hbimpg  40427  hbexg  40429  ax6e2nd  40431  hbimpgVD  40777  ax6e2eqVD  40780  ax6e2ndVD  40781  ax6e2ndALT  40803  absnsb  42778  rexrsb  42814  ichal  43109  setrec1lem2  44271  setrec1lem4  44273