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  2073  spsbbi  2076  hbal  2170  hbsbwOLD  2175  nfim1  2202  axc4  2322  axc16i  2436  sb4a  2480  dfmoeu  2531  nexmo  2536  moimi  2540  eu6  2569  darii  2660  cesare  2667  camestres  2668  festino  2669  baroco  2671  darapti  2679  calemes  2682  fesapo  2686  eqeq1d  2733  ralimi2  3064  rgen2a  3337  rmoeq1  3377  ceqsal1t  3469  spcgft  3504  vtoclgft  3507  rspct  3563  elabgt  3627  elabgtOLD  3628  elabgtOLDOLD  3629  reu6  3685  sbciegftOLD  3779  csbeq2  3855  ssrmof  4002  ralss  4009  rabss2  4028  csbnestgfw  4372  csbnestgf  4377  undif4  4417  ralidmw  4458  ralidm  4462  ralf0  4464  falseral0  4466  intmin4  4927  dfiin2g  4981  invdisj  5077  disjss3  5090  axrep2  5220  sepex  5238  ax6vsep  5241  axnul  5243  csbexg  5248  axpow3  5306  nfnid  5313  axprALT  5360  axprlem1  5361  axprlem4  5364  axprlem4OLD  5367  axprlem5OLD  5368  axprOLD  5369  ssrelrel  5736  iresn0n0  6003  iotanul  6461  iota4  6462  fundif  6530  fv3  6840  zfrep6  7887  ssfi  9082  elirrv  9483  dfom3  9537  dfac5  10017  dfac2a  10018  dfac2b  10019  kmlem13  10051  zorng  10392  brdom3  10416  brdom4  10418  axpowndlem2  10486  axregnd  10492  axacndlem1  10495  axacndlem2  10496  axacndlem3  10497  axacndlem4  10498  axacnd  10500  ingru  10703  dfnn2  12135  trclfvcotr  14913  prodeq2w  15814  2ndcdisj2  23370  elons2  28193  dfn0s2  28258  pjnormssi  32143  disjin  32561  disjin2  32562  ssdifidlprm  33418  bnj1172  35008  bnj1174  35010  bnj1176  35012  bnj1523  35078  axsepg2  35089  axsepg2ALT  35090  r1omhfbregs  35121  fineqvpow  35126  elpotr  35814  dfon2lem8  35823  distel  35836  hbimtg  35839  bj-gl4  36628  bj-alanim  36645  bj-2albi  36646  bj-exalim  36665  bj-cbvalimt  36672  bj-cbveximt  36673  bj-eximALT  36674  bj-aleximiALT  36675  bj-ssbid2ALT  36696  bj-sb  36720  bj-hbext  36743  bj-nfalt  36744  bj-nfext  36745  bj-nnfalt  36799  bj-nnfext  36800  bj-cbv3tb  36820  bj-nfs1t2  36824  bj-hbaeb2  36851  bj-equsal1  36857  bj-equsal2  36858  2stdpc5  36862  bj-ceqsalt0  36917  bj-ceqsalt1  36918  bj-abv  36939  bj-bm1.3ii  37097  exrecfnlem  37412  wl-moae  37549  wl-aleq  37568  wl-sb8ft  37583  wl-sb8eft  37584  wl-lem-nexmo  37600  wl-axc11rc11  37616  phpreu  37643  nninfnub  37790  mpobi123f  38201  eqab2  38282  trcoss  38518  hba1-o  38935  aecom-o  38939  ax12fromc15  38943  hbequid  38947  axc711  38952  axc711toc7  38954  axc711to11  38955  axc5c711  38956  axc5c711toc7  38958  axc5c711to11  38959  equidqe  38960  equid1ALT  38963  axc11nfromc11  38964  axc11n-16  38976  ax12eq  38979  ax12el  38980  ax12indi  38982  eu6w  42708  dfac11  43094  intimag  43688  intimasn  43689  frege70  43965  pm11.12  44407  2albi  44410  2exbi  44412  pm11.57  44421  pm11.61  44425  axc5c4c711toc7  44436  axc5c4c711to11  44437  axc11next  44438  pm13.192  44442  ralbidar  44476  rexbidar  44477  hbntal  44585  hbimpg  44586  hbexg  44588  ax6e2nd  44590  hbimpgVD  44935  ax6e2eqVD  44938  ax6e2ndVD  44939  ax6e2ndALT  44961  ssclaxsep  45014  absnsb  47057  rexrsb  47130  ichal  47496  setrec1lem2  49719  setrec1lem4  49721