Theorem alimi 1508

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
alimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alimi	⊢ (∀𝑥𝜑 → ∀𝑥𝜓)

Proof of Theorem alimi

Step	Hyp	Ref	Expression
1		ax-5 1500	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2		alimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1504	1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1400

This theorem was proved from axioms:  ax-mp 5  ax-5 1500  ax-gen 1502

This theorem is referenced by:  2alimi  1509  al2imi  1511  alrimih  1522  hbal  1530  19.26  1534  19.33  1537  hbequid  1566  equidqe  1585  hbim  1598  hbor  1599  nford  1620  nfand  1621  nfal  1629  nfalt  1631  19.21ht  1634  exbi  1657  19.29  1673  19.25  1679  alexim  1698  alexnim  1701  19.9hd  1714  19.32r  1732  ax10  1769  spimh  1790  equvini  1811  nfexd  1814  stdpc4  1828  ax10oe  1850  sbcof2  1863  sb4bor  1888  nfsb2or  1890  spsbim  1896  ax16i  1911  sbi2v  1947  nfsbt  2036  nfsbd  2037  sbalyz  2059  hbsb4t  2073  dvelimor  2078  sbal2  2080  mo2n  2114  eumo0  2117  mor  2129  bm1.1  2223  alral  2595  rgen2a  2604  ralimi2  2610  rexim  2644  r19.32r  2697  ceqsalt  2848  spcgft  2902  spcegft  2904  spc2gv  2916  spc3gv  2918  rspct  2922  elabgt  2967  reu6  3015  sbciegft  3082  csbeq2  3171  csbnestgf  3200  ssrmof  3311  rabss2  3331  undif4  3587  ssdif0im  3589  inssdif0imOLD  3593  ssundifim  3611  ralf0  3630  ralm  3631  intmin4  3996  dfiin2g  4043  invdisj  4121  trint  4242  a9evsep  4253  axnul  4256  csbexga  4259  exmidn0m  4336  exmidsssn  4337  exmidsssnc  4338  exmid0el  4339  ordunisuc2r  4659  tfi  4727  peano5  4743  ssrelrel  4873  issref  5168  iotanul  5351  iota4  5355  dffun5r  5387  fundif  5423  fv3  5716  mptfvex  5788  ssoprab2  6138  mpofvex  6435  tfri1dALT  6616  prodeq2w  12306  bj-nfalt  16775  elabgft1  16789  bj-rspgt  16797  bj-axemptylem  16901  bj-indind  16941  setindis  16976  bdsetindis  16978  bj-inf2vnlem1  16979  bj-inf2vn  16983  bj-inf2vn2  16984  als-no-surprise  17121