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 1535

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  1823  19.38  1839  19.26  1871  19.33  1885  alcomiw  2050  alcomiwOLD  2051  hba1w  2054  hbalw  2056  naev2  2066  2stdpc4  2075  spsbbi  2078  hbal  2174  nfim1  2199  sbequ2OLD  2251  axc4  2340  axc16i  2458  sb4a  2509  dfmoeu  2618  nexmo  2623  moimi  2627  eu6  2659  darii  2750  cesare  2757  camestres  2758  festino  2759  baroco  2761  darapti  2769  calemes  2772  fesapo  2776  eqeq1d  2823  ralimi2  3157  rgen2a  3229  ceqsalt  3527  spcgft  3587  rspct  3609  elabgt  3663  reu6  3717  sbciegft  3808  csbeq2  3888  ssrmof  4032  rabss2  4054  csbnestgfw  4371  csbnestgf  4376  undif4  4416  falseral0  4459  intmin4  4905  dfiin2g  4957  invdisj  5050  disjss3  5065  axrep2  5193  ax6vsep  5207  axnul  5209  csbexg  5214  nfnid  5276  axprALT  5323  axprlem1  5324  axprlem4  5327  axprlem5  5328  axpr  5329  ssrelrel  5669  iresn0n0  5923  iotanul  6333  iota4  6336  fundif  6403  fv3  6688  zfrep6  7656  dfom3  9110  dfac5  9554  dfac2a  9555  dfac2b  9556  kmlem13  9588  zorng  9926  brdom3  9950  brdom4  9952  axpowndlem2  10020  axregnd  10026  axacndlem1  10029  axacndlem2  10030  axacndlem3  10031  axacndlem4  10032  axacnd  10034  ingru  10237  dfnn2  11651  trclfvcotr  14369  prodeq2w  15266  2ndcdisj2  22065  pjnormssi  29945  disjin  30336  disjin2  30337  bnj1172  32273  bnj1174  32275  bnj1176  32277  bnj1523  32343  elpotr  33026  dfon2lem8  33035  distel  33048  hbimtg  33051  bj-gl4  33929  bj-alanim  33946  bj-2albi  33947  bj-exalim  33965  bj-cbvalimt  33972  bj-cbveximt  33973  bj-eximALT  33974  bj-aleximiALT  33975  bj-ssbid2ALT  33996  bj-sb  34021  bj-hbext  34044  bj-nfalt  34045  bj-nfext  34046  bj-nnfalt  34095  bj-nnfext  34096  bj-cbv3tb  34109  bj-nfs1t2  34113  bj-hbaeb2  34141  bj-equsal1  34147  bj-equsal2  34148  2stdpc5  34152  bj-ceqsalt0  34203  bj-ceqsalt1  34204  bj-bm1.3ii  34360  exrecfnlem  34663  wl-moae  34771  wl-aleq  34790  wl-lem-nexmo  34818  wl-axc11rc11  34830  phpreu  34891  nninfnub  35041  mpobi123f  35455  trcoss  35737  hba1-o  36048  aecom-o  36052  ax12fromc15  36056  hbequid  36060  axc711  36065  axc711toc7  36067  axc711to11  36068  axc5c711  36069  axc5c711toc7  36071  axc5c711to11  36072  equidqe  36073  equid1ALT  36076  axc11nfromc11  36077  axc11n-16  36089  ax12eq  36092  ax12el  36093  ax12indi  36095  dfac11  39682  intimag  40021  intimasn  40022  frege70  40299  pm11.12  40727  2albi  40730  2exbi  40732  pm11.57  40741  pm11.61  40745  axc5c4c711toc7  40756  axc5c4c711to11  40757  axc11next  40758  pm13.192  40762  ralbidar  40797  rexbidar  40798  hbntal  40907  hbimpg  40908  hbexg  40910  ax6e2nd  40912  hbimpgVD  41258  ax6e2eqVD  41261  ax6e2ndVD  41262  ax6e2ndALT  41284  absnsb  43282  rexrsb  43318  ichal  43647  setrec1lem2  44811  setrec1lem4  44813