Theorem alimi 1412

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

Syntax hints:   → wi 4  ∀wal 1310

This theorem was proved from axioms:  ax-mp 7  ax-5 1404  ax-gen 1406

This theorem is referenced by:  2alimi  1413  al2imi  1415  alrimih  1426  hbal  1434  19.26  1438  19.33  1441  hbequid  1474  equidqe  1493  hbim  1505  hbor  1506  nford  1527  nfand  1528  nfalt  1538  19.21ht  1541  exbi  1564  19.29  1580  19.25  1586  alexim  1605  alexnim  1608  19.9hd  1621  19.32r  1639  ax10  1676  spimh  1696  equvini  1712  nfexd  1715  stdpc4  1729  ax10oe  1749  sbcof2  1762  sb4bor  1787  nfsb2or  1789  spsbim  1795  ax16i  1810  sbi2v  1844  nfsbt  1923  nfsbd  1924  sbalyz  1948  hbsb4t  1962  dvelimor  1967  sbal2  1971  mo2n  2001  eumo0  2004  mor  2015  bm1.1  2098  alral  2450  rgen2a  2458  ralimi2  2464  rexim  2498  r19.32r  2550  ceqsalt  2681  spcgft  2732  spcegft  2734  spc2gv  2745  spc3gv  2747  rspct  2751  elabgt  2793  reu6  2840  sbciegft  2905  csbnestgf  3016  ssrmof  3124  rabss2  3144  rabxmdc  3358  undif4  3389  ssdif0im  3391  inssdif0im  3394  ssundifim  3410  ralf0  3430  ralm  3431  intmin4  3763  dfiin2g  3810  invdisj  3887  trint  3999  a9evsep  4008  axnul  4011  csbexga  4014  exmidn0m  4082  exmidsssn  4083  exmidsssnc  4084  exmid0el  4085  ordunisuc2r  4388  tfi  4454  peano5  4470  ssrelrel  4597  issref  4877  iotanul  5059  iota4  5062  dffun5r  5091  fv3  5396  mptfvex  5458  ssoprab2  5779  mpofvex  6053  tfri1dALT  6200  bj-nfalt  12655  elabgft1  12668  bj-rspgt  12676  bj-axemptylem  12773  bj-indind  12813  setindis  12848  bdsetindis  12850  bj-inf2vnlem1  12851  bj-inf2vn  12855  bj-inf2vn2  12856