Theorem alimi 1811

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-gen 1795  ax-4 1809

This theorem is referenced by:  2alimi  1812  ala1  1813  sylg  1823  19.38  1839  19.26  1870  19.33  1884  alcomimw  2043  hba1w  2048  hbalw  2050  exexw  2052  naev2  2062  2stdpc4  2071  spsbbi  2074  hbal  2168  hbsbwOLD  2173  nfim1  2200  axc4  2322  axc16i  2441  sb4a  2485  dfmoeu  2536  nexmo  2541  moimi  2545  eu6  2574  darii  2665  cesare  2672  camestres  2673  festino  2674  baroco  2676  darapti  2684  calemes  2687  fesapo  2691  eqeq1d  2738  ralimi2  3069  rgen2a  3355  rmoeq1  3400  ceqsal1t  3498  spcgft  3533  vtoclgft  3536  rspct  3592  elabgt  3656  elabgtOLD  3657  reu6  3714  sbciegftOLD  3808  csbeq2  3884  ssrmof  4031  ralss  4038  rabss2  4058  csbnestgfw  4402  csbnestgf  4407  undif4  4447  ralidmw  4488  ralidm  4492  ralf0  4494  falseral0  4496  intmin4  4958  dfiin2g  5013  invdisj  5110  disjss3  5123  axrep2  5257  sepex  5275  ax6vsep  5278  axnul  5280  csbexg  5285  axpow3  5343  nfnid  5350  axprALT  5397  axprlem1  5398  axprlem4  5401  axprlem4OLD  5404  axprlem5OLD  5405  axprOLD  5406  ssrelrel  5780  iresn0n0  6046  iotanul  6514  iota4  6517  fundif  6590  fv3  6899  zfrep6  7958  ssfi  9192  dfom3  9666  dfac5  10148  dfac2a  10149  dfac2b  10150  kmlem13  10182  zorng  10523  brdom3  10547  brdom4  10549  axpowndlem2  10617  axregnd  10623  axacndlem1  10626  axacndlem2  10627  axacndlem3  10628  axacndlem4  10629  axacnd  10631  ingru  10834  dfnn2  12258  trclfvcotr  15033  prodeq2w  15931  2ndcdisj2  23400  elons2  28216  dfn0s2  28281  pjnormssi  32154  disjin  32572  disjin2  32573  ssdifidlprm  33478  bnj1172  35037  bnj1174  35039  bnj1176  35041  bnj1523  35107  axsepg2  35118  axsepg2ALT  35119  fineqvpow  35132  elpotr  35804  dfon2lem8  35813  distel  35826  hbimtg  35829  bj-gl4  36618  bj-alanim  36635  bj-2albi  36636  bj-exalim  36655  bj-cbvalimt  36662  bj-cbveximt  36663  bj-eximALT  36664  bj-aleximiALT  36665  bj-ssbid2ALT  36686  bj-sb  36710  bj-hbext  36733  bj-nfalt  36734  bj-nfext  36735  bj-nnfalt  36789  bj-nnfext  36790  bj-cbv3tb  36810  bj-nfs1t2  36814  bj-hbaeb2  36841  bj-equsal1  36847  bj-equsal2  36848  2stdpc5  36852  bj-ceqsalt0  36907  bj-ceqsalt1  36908  bj-abv  36929  bj-bm1.3ii  37087  exrecfnlem  37402  wl-moae  37539  wl-aleq  37558  wl-sb8ft  37573  wl-sb8eft  37574  wl-lem-nexmo  37590  wl-axc11rc11  37606  phpreu  37633  nninfnub  37780  mpobi123f  38191  trcoss  38505  hba1-o  38920  aecom-o  38924  ax12fromc15  38928  hbequid  38932  axc711  38937  axc711toc7  38939  axc711to11  38940  axc5c711  38941  axc5c711toc7  38943  axc5c711to11  38944  equidqe  38945  equid1ALT  38948  axc11nfromc11  38949  axc11n-16  38961  ax12eq  38964  ax12el  38965  ax12indi  38967  eu6w  42674  dfac11  43061  intimag  43655  intimasn  43656  frege70  43932  pm11.12  44374  2albi  44377  2exbi  44379  pm11.57  44388  pm11.61  44392  axc5c4c711toc7  44403  axc5c4c711to11  44404  axc11next  44405  pm13.192  44409  ralbidar  44444  rexbidar  44445  hbntal  44553  hbimpg  44554  hbexg  44556  ax6e2nd  44558  hbimpgVD  44903  ax6e2eqVD  44906  ax6e2ndVD  44907  ax6e2ndALT  44929  ssclaxsep  44982  absnsb  47036  rexrsb  47109  ichal  47460  setrec1lem2  49532  setrec1lem4  49534