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  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  5795  iresn0n0  6052  iotanul  6519  iota4  6522  fundif  6595  fv3  6907  zfrep6  7938  ssfi  9170  dfom3  9639  dfac5  10120  dfac2a  10121  dfac2b  10122  kmlem13  10154  zorng  10496  brdom3  10520  brdom4  10522  axpowndlem2  10590  axregnd  10596  axacndlem1  10599  axacndlem2  10600  axacndlem3  10601  axacndlem4  10602  axacnd  10604  ingru  10807  dfnn2  12222  trclfvcotr  14953  prodeq2w  15853  2ndcdisj2  22953  pjnormssi  31409  disjin  31805  disjin2  31806  bnj1172  34001  bnj1174  34003  bnj1176  34005  bnj1523  34071  fineqvpow  34085  elpotr  34742  dfon2lem8  34751  distel  34764  hbimtg  34767  bj-gl4  35462  bj-alanim  35479  bj-2albi  35480  bj-exalim  35498  bj-cbvalimt  35505  bj-cbveximt  35506  bj-eximALT  35507  bj-aleximiALT  35508  bj-ssbid2ALT  35529  bj-sb  35554  bj-hbext  35577  bj-nfalt  35578  bj-nfext  35579  bj-nnfalt  35633  bj-nnfext  35634  bj-cbv3tb  35654  bj-nfs1t2  35658  bj-hbaeb2  35685  bj-equsal1  35691  bj-equsal2  35692  2stdpc5  35696  bj-ceqsalt0  35753  bj-ceqsalt1  35754  bj-abv  35775  bj-bm1.3ii  35934  exrecfnlem  36249  wl-moae  36374  wl-aleq  36393  wl-lem-nexmo  36421  wl-axc11rc11  36434  phpreu  36461  nninfnub  36608  mpobi123f  37019  trcoss  37341  hba1-o  37756  aecom-o  37760  ax12fromc15  37764  hbequid  37768  axc711  37773  axc711toc7  37775  axc711to11  37776  axc5c711  37777  axc5c711toc7  37779  axc5c711to11  37780  equidqe  37781  equid1ALT  37784  axc11nfromc11  37785  axc11n-16  37797  ax12eq  37800  ax12el  37801  ax12indi  37803  dfac11  41790  intimag  42393  intimasn  42394  frege70  42670  pm11.12  43120  2albi  43123  2exbi  43125  pm11.57  43134  pm11.61  43138  axc5c4c711toc7  43149  axc5c4c711to11  43150  axc11next  43151  pm13.192  43155  ralbidar  43190  rexbidar  43191  hbntal  43300  hbimpg  43301  hbexg  43303  ax6e2nd  43305  hbimpgVD  43651  ax6e2eqVD  43654  ax6e2ndVD  43655  ax6e2ndALT  43677  absnsb  45724  rexrsb  45795  ichal  46121  setrec1lem2  47687  setrec1lem4  47689