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 1538

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  1872  19.33  1886  alcomiw  2045  hba1w  2049  hbalw  2051  exexw  2053  naev2  2063  2stdpc4  2072  spsbbi  2075  hbal  2166  hbsbw  2168  nfim1  2191  axc4  2313  axc16i  2434  sb4a  2478  dfmoeu  2529  nexmo  2534  moimi  2538  eu6  2567  darii  2659  cesare  2666  camestres  2667  festino  2668  baroco  2670  darapti  2678  calemes  2681  fesapo  2685  eqeq1d  2733  ralimi2  3077  raleleq  3336  rgen2a  3366  rmoeq1  3413  ceqsal1t  3504  spcgft  3578  rspct  3598  elabgt  3662  elabgtOLD  3663  reu6  3722  sbciegft  3815  csbeq2  3898  ssrmof  4049  rabss2  4075  csbnestgfw  4419  csbnestgf  4424  undif4  4466  ralidmw  4507  ralidm  4511  ralf0  4513  falseral0  4519  intmin4  4981  dfiin2g  5035  invdisj  5132  disjss3  5147  axrep2  5288  ax6vsep  5303  axnul  5305  csbexg  5310  nfnid  5373  axprALT  5420  axprlem1  5421  axprlem4  5424  axprlem5  5425  axpr  5426  ssrelrel  5796  iresn0n0  6053  iotanul  6521  iota4  6524  fundif  6597  fv3  6909  zfrep6  7945  ssfi  9179  dfom3  9648  dfac5  10129  dfac2a  10130  dfac2b  10131  kmlem13  10163  zorng  10505  brdom3  10529  brdom4  10531  axpowndlem2  10599  axregnd  10605  axacndlem1  10608  axacndlem2  10609  axacndlem3  10610  axacndlem4  10611  axacnd  10613  ingru  10816  dfnn2  12232  trclfvcotr  14963  prodeq2w  15863  2ndcdisj2  23281  elons2  28064  dfn0s2  28085  pjnormssi  31854  disjin  32250  disjin2  32251  bnj1172  34476  bnj1174  34478  bnj1176  34480  bnj1523  34546  fineqvpow  34560  elpotr  35223  dfon2lem8  35232  distel  35245  hbimtg  35248  bj-gl4  35937  bj-alanim  35954  bj-2albi  35955  bj-exalim  35973  bj-cbvalimt  35980  bj-cbveximt  35981  bj-eximALT  35982  bj-aleximiALT  35983  bj-ssbid2ALT  36004  bj-sb  36029  bj-hbext  36052  bj-nfalt  36053  bj-nfext  36054  bj-nnfalt  36108  bj-nnfext  36109  bj-cbv3tb  36129  bj-nfs1t2  36133  bj-hbaeb2  36160  bj-equsal1  36166  bj-equsal2  36167  2stdpc5  36171  bj-ceqsalt0  36228  bj-ceqsalt1  36229  bj-abv  36250  bj-bm1.3ii  36409  exrecfnlem  36724  wl-moae  36849  wl-aleq  36868  wl-lem-nexmo  36896  wl-axc11rc11  36909  phpreu  36936  nninfnub  37083  mpobi123f  37494  trcoss  37816  hba1-o  38231  aecom-o  38235  ax12fromc15  38239  hbequid  38243  axc711  38248  axc711toc7  38250  axc711to11  38251  axc5c711  38252  axc5c711toc7  38254  axc5c711to11  38255  equidqe  38256  equid1ALT  38259  axc11nfromc11  38260  axc11n-16  38272  ax12eq  38275  ax12el  38276  ax12indi  38278  dfac11  42267  intimag  42870  intimasn  42871  frege70  43147  pm11.12  43597  2albi  43600  2exbi  43602  pm11.57  43611  pm11.61  43615  axc5c4c711toc7  43626  axc5c4c711to11  43627  axc11next  43628  pm13.192  43632  ralbidar  43667  rexbidar  43668  hbntal  43777  hbimpg  43778  hbexg  43780  ax6e2nd  43782  hbimpgVD  44128  ax6e2eqVD  44131  ax6e2ndVD  44132  ax6e2ndALT  44154  absnsb  46196  rexrsb  46267  ichal  46593  setrec1lem2  47895  setrec1lem4  47897