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  1992  nfsbd  1993  sbalyz  2015  hbsb4t  2029  dvelimor  2034  sbal2  2036  mo2n  2070  eumo0  2073  mor  2084  bm1.1  2178  alral  2539  rgen2a  2548  ralimi2  2554  rexim  2588  r19.32r  2640  ceqsalt  2786  spcgft  2838  spcegft  2840  spc2gv  2852  spc3gv  2854  rspct  2858  elabgt  2902  reu6  2950  sbciegft  3017  csbeq2  3105  csbnestgf  3134  ssrmof  3243  rabss2  3263  rabxmdc  3479  undif4  3510  ssdif0im  3512  inssdif0im  3515  ssundifim  3531  ralf0  3550  ralm  3551  intmin4  3899  dfiin2g  3946  invdisj  4024  trint  4143  a9evsep  4152  axnul  4155  csbexga  4158  exmidn0m  4231  exmidsssn  4232  exmidsssnc  4233  exmid0el  4234  ordunisuc2r  4547  tfi  4615  peano5  4631  ssrelrel  4760  issref  5049  iotanul  5231  iota4  5235  dffun5r  5267  fv3  5578  mptfvex  5644  ssoprab2  5975  mpofvex  6260  tfri1dALT  6406  prodeq2w  11702  bj-nfalt  15326  elabgft1  15340  bj-rspgt  15348  bj-axemptylem  15454  bj-indind  15494  setindis  15529  bdsetindis  15531  bj-inf2vnlem1  15532  bj-inf2vn  15536  bj-inf2vn2  15537