Theorem alimi 1466

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

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-5 1458  ax-gen 1460

This theorem is referenced by:  2alimi  1467  al2imi  1469  alrimih  1480  hbal  1488  19.26  1492  19.33  1495  hbequid  1524  equidqe  1543  hbim  1556  hbor  1557  nford  1578  nfand  1579  nfal  1587  nfalt  1589  19.21ht  1592  exbi  1615  19.29  1631  19.25  1637  alexim  1656  alexnim  1659  19.9hd  1673  19.32r  1691  ax10  1728  spimh  1748  equvini  1769  nfexd  1772  stdpc4  1786  ax10oe  1808  sbcof2  1821  sb4bor  1846  nfsb2or  1848  spsbim  1854  ax16i  1869  sbi2v  1904  nfsbt  1988  nfsbd  1989  sbalyz  2011  hbsb4t  2025  dvelimor  2030  sbal2  2032  mo2n  2066  eumo0  2069  mor  2080  bm1.1  2174  alral  2535  rgen2a  2544  ralimi2  2550  rexim  2584  r19.32r  2636  ceqsalt  2778  spcgft  2829  spcegft  2831  spc2gv  2843  spc3gv  2845  rspct  2849  elabgt  2893  reu6  2941  sbciegft  3008  csbeq2  3096  csbnestgf  3124  ssrmof  3233  rabss2  3253  rabxmdc  3469  undif4  3500  ssdif0im  3502  inssdif0im  3505  ssundifim  3521  ralf0  3541  ralm  3542  intmin4  3887  dfiin2g  3934  invdisj  4012  trint  4131  a9evsep  4140  axnul  4143  csbexga  4146  exmidn0m  4219  exmidsssn  4220  exmidsssnc  4221  exmid0el  4222  ordunisuc2r  4531  tfi  4599  peano5  4615  ssrelrel  4744  issref  5029  iotanul  5211  iota4  5215  dffun5r  5247  fv3  5557  mptfvex  5622  ssoprab2  5953  mpofvex  6229  tfri1dALT  6377  prodeq2w  11599  bj-nfalt  14994  elabgft1  15008  bj-rspgt  15016  bj-axemptylem  15122  bj-indind  15162  setindis  15197  bdsetindis  15199  bj-inf2vnlem1  15200  bj-inf2vn  15204  bj-inf2vn2  15205