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  2837  spcegft  2839  spc2gv  2851  spc3gv  2853  rspct  2857  elabgt  2901  reu6  2949  sbciegft  3016  csbeq2  3104  csbnestgf  3133  ssrmof  3242  rabss2  3262  rabxmdc  3478  undif4  3509  ssdif0im  3511  inssdif0im  3514  ssundifim  3530  ralf0  3549  ralm  3550  intmin4  3898  dfiin2g  3945  invdisj  4023  trint  4142  a9evsep  4151  axnul  4154  csbexga  4157  exmidn0m  4230  exmidsssn  4231  exmidsssnc  4232  exmid0el  4233  ordunisuc2r  4546  tfi  4614  peano5  4630  ssrelrel  4759  issref  5048  iotanul  5230  iota4  5234  dffun5r  5266  fv3  5577  mptfvex  5643  ssoprab2  5974  mpofvex  6256  tfri1dALT  6404  prodeq2w  11699  bj-nfalt  15256  elabgft1  15270  bj-rspgt  15278  bj-axemptylem  15384  bj-indind  15424  setindis  15459  bdsetindis  15461  bj-inf2vnlem1  15462  bj-inf2vn  15466  bj-inf2vn2  15467