Theorem alimi 1815

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-gen 1799  ax-4 1813

This theorem is referenced by:  2alimi  1816  ala1  1817  sylg  1826  19.38  1842  19.26  1874  19.33  1888  alcomiw  2047  alcomiwOLD  2048  hba1w  2051  hbalw  2053  exexw  2055  naev2  2065  2stdpc4  2074  spsbbi  2077  hbal  2169  hbsbw  2171  nfim1  2195  sbequ2OLD  2245  axc4  2319  axc16i  2436  sb4a  2484  dfmoeu  2536  nexmo  2541  moimi  2545  eu6  2574  darii  2666  cesare  2673  camestres  2674  festino  2675  baroco  2677  darapti  2685  calemes  2688  fesapo  2692  eqeq1d  2740  ralimi2  3083  rgen2a  3155  ceqsalt  3452  spcgft  3517  rspct  3537  elabgt  3596  elabgtOLD  3597  reu6  3656  sbciegft  3749  csbeq2  3833  ssrmof  3982  rabss2  4007  csbnestgfw  4350  csbnestgf  4355  undif4  4397  ralidmw  4435  ralidm  4439  ralf0  4441  falseral0  4447  intmin4  4905  dfiin2g  4958  invdisj  5054  disjss3  5069  axrep2  5208  ax6vsep  5222  axnul  5224  csbexg  5229  nfnid  5293  axprALT  5340  axprlem1  5341  axprlem4  5344  axprlem5  5345  axpr  5346  ssrelrel  5695  iresn0n0  5952  iotanul  6396  iota4  6399  fundif  6467  fv3  6774  zfrep6  7771  ssfi  8918  dfom3  9335  dfac5  9815  dfac2a  9816  dfac2b  9817  kmlem13  9849  zorng  10191  brdom3  10215  brdom4  10217  axpowndlem2  10285  axregnd  10291  axacndlem1  10294  axacndlem2  10295  axacndlem3  10296  axacndlem4  10297  axacnd  10299  ingru  10502  dfnn2  11916  trclfvcotr  14648  prodeq2w  15550  2ndcdisj2  22516  pjnormssi  30431  disjin  30826  disjin2  30827  bnj1172  32881  bnj1174  32883  bnj1176  32885  bnj1523  32951  fineqvpow  32965  elpotr  33663  dfon2lem8  33672  distel  33685  hbimtg  33688  bj-gl4  34704  bj-alanim  34721  bj-2albi  34722  bj-exalim  34740  bj-cbvalimt  34747  bj-cbveximt  34748  bj-eximALT  34749  bj-aleximiALT  34750  bj-ssbid2ALT  34771  bj-sb  34796  bj-hbext  34819  bj-nfalt  34820  bj-nfext  34821  bj-nnfalt  34875  bj-nnfext  34876  bj-cbv3tb  34896  bj-nfs1t2  34900  bj-hbaeb2  34928  bj-equsal1  34934  bj-equsal2  34935  2stdpc5  34939  bj-ceqsalt0  34996  bj-ceqsalt1  34997  bj-abv  35018  bj-bm1.3ii  35162  exrecfnlem  35477  wl-moae  35602  wl-aleq  35621  wl-lem-nexmo  35649  wl-axc11rc11  35661  phpreu  35688  nninfnub  35836  mpobi123f  36247  trcoss  36527  hba1-o  36838  aecom-o  36842  ax12fromc15  36846  hbequid  36850  axc711  36855  axc711toc7  36857  axc711to11  36858  axc5c711  36859  axc5c711toc7  36861  axc5c711to11  36862  equidqe  36863  equid1ALT  36866  axc11nfromc11  36867  axc11n-16  36879  ax12eq  36882  ax12el  36883  ax12indi  36885  dfac11  40803  intimag  41153  intimasn  41154  frege70  41430  pm11.12  41882  2albi  41885  2exbi  41887  pm11.57  41896  pm11.61  41900  axc5c4c711toc7  41911  axc5c4c711to11  41912  axc11next  41913  pm13.192  41917  ralbidar  41952  rexbidar  41953  hbntal  42062  hbimpg  42063  hbexg  42065  ax6e2nd  42067  hbimpgVD  42413  ax6e2eqVD  42416  ax6e2ndVD  42417  ax6e2ndALT  42439  absnsb  44408  rexrsb  44479  ichal  44806  setrec1lem2  46280  setrec1lem4  46282