Theorem alimi 1814

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-gen 1798  ax-4 1812

This theorem is referenced by:  2alimi  1815  ala1  1816  sylg  1826  19.38  1842  19.26  1874  19.33  1888  alcomiw  2047  hba1w  2051  hbalw  2053  exexw  2055  naev2  2065  2stdpc4  2074  spsbbi  2077  hbal  2168  hbsbw  2170  nfim1  2193  axc4  2315  axc16i  2436  sb4a  2480  dfmoeu  2531  nexmo  2536  moimi  2540  eu6  2569  darii  2661  cesare  2668  camestres  2669  festino  2670  baroco  2672  darapti  2680  calemes  2683  fesapo  2687  eqeq1d  2735  ralimi2  3079  raleleq  3338  rgen2a  3368  rmoeq1  3415  ceqsal1t  3505  spcgft  3579  rspct  3599  elabgt  3663  elabgtOLD  3664  reu6  3723  sbciegft  3816  csbeq2  3899  ssrmof  4050  rabss2  4076  csbnestgfw  4420  csbnestgf  4425  undif4  4467  ralidmw  4508  ralidm  4512  ralf0  4514  falseral0  4520  intmin4  4982  dfiin2g  5036  invdisj  5133  disjss3  5148  axrep2  5289  ax6vsep  5304  axnul  5306  csbexg  5311  nfnid  5374  axprALT  5421  axprlem1  5422  axprlem4  5425  axprlem5  5426  axpr  5427  ssrelrel  5797  iresn0n0  6054  iotanul  6522  iota4  6525  fundif  6598  fv3  6910  zfrep6  7941  ssfi  9173  dfom3  9642  dfac5  10123  dfac2a  10124  dfac2b  10125  kmlem13  10157  zorng  10499  brdom3  10523  brdom4  10525  axpowndlem2  10593  axregnd  10599  axacndlem1  10602  axacndlem2  10603  axacndlem3  10604  axacndlem4  10605  axacnd  10607  ingru  10810  dfnn2  12225  trclfvcotr  14956  prodeq2w  15856  2ndcdisj2  22961  pjnormssi  31421  disjin  31817  disjin2  31818  bnj1172  34012  bnj1174  34014  bnj1176  34016  bnj1523  34082  fineqvpow  34096  elpotr  34753  dfon2lem8  34762  distel  34775  hbimtg  34778  bj-gl4  35473  bj-alanim  35490  bj-2albi  35491  bj-exalim  35509  bj-cbvalimt  35516  bj-cbveximt  35517  bj-eximALT  35518  bj-aleximiALT  35519  bj-ssbid2ALT  35540  bj-sb  35565  bj-hbext  35588  bj-nfalt  35589  bj-nfext  35590  bj-nnfalt  35644  bj-nnfext  35645  bj-cbv3tb  35665  bj-nfs1t2  35669  bj-hbaeb2  35696  bj-equsal1  35702  bj-equsal2  35703  2stdpc5  35707  bj-ceqsalt0  35764  bj-ceqsalt1  35765  bj-abv  35786  bj-bm1.3ii  35945  exrecfnlem  36260  wl-moae  36385  wl-aleq  36404  wl-lem-nexmo  36432  wl-axc11rc11  36445  phpreu  36472  nninfnub  36619  mpobi123f  37030  trcoss  37352  hba1-o  37767  aecom-o  37771  ax12fromc15  37775  hbequid  37779  axc711  37784  axc711toc7  37786  axc711to11  37787  axc5c711  37788  axc5c711toc7  37790  axc5c711to11  37791  equidqe  37792  equid1ALT  37795  axc11nfromc11  37796  axc11n-16  37808  ax12eq  37811  ax12el  37812  ax12indi  37814  dfac11  41804  intimag  42407  intimasn  42408  frege70  42684  pm11.12  43134  2albi  43137  2exbi  43139  pm11.57  43148  pm11.61  43152  axc5c4c711toc7  43163  axc5c4c711to11  43164  axc11next  43165  pm13.192  43169  ralbidar  43204  rexbidar  43205  hbntal  43314  hbimpg  43315  hbexg  43317  ax6e2nd  43319  hbimpgVD  43665  ax6e2eqVD  43668  ax6e2ndVD  43669  ax6e2ndALT  43691  absnsb  45737  rexrsb  45808  ichal  46134  setrec1lem2  47733  setrec1lem4  47735