Theorem alimi 1501

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

Syntax hints:   → wi 4  ∀wal 1393

This theorem was proved from axioms:  ax-mp 5  ax-5 1493  ax-gen 1495

This theorem is referenced by:  2alimi  1502  al2imi  1504  alrimih  1515  hbal  1523  19.26  1527  19.33  1530  hbequid  1559  equidqe  1578  hbim  1591  hbor  1592  nford  1613  nfand  1614  nfal  1622  nfalt  1624  19.21ht  1627  exbi  1650  19.29  1666  19.25  1672  alexim  1691  alexnim  1694  19.9hd  1708  19.32r  1726  ax10  1763  spimh  1783  equvini  1804  nfexd  1807  stdpc4  1821  ax10oe  1843  sbcof2  1856  sb4bor  1881  nfsb2or  1883  spsbim  1889  ax16i  1904  sbi2v  1939  nfsbt  2027  nfsbd  2028  sbalyz  2050  hbsb4t  2064  dvelimor  2069  sbal2  2071  mo2n  2105  eumo0  2108  mor  2120  bm1.1  2214  alral  2575  rgen2a  2584  ralimi2  2590  rexim  2624  r19.32r  2677  ceqsalt  2826  spcgft  2880  spcegft  2882  spc2gv  2894  spc3gv  2896  rspct  2900  elabgt  2944  reu6  2992  sbciegft  3059  csbeq2  3148  csbnestgf  3177  ssrmof  3287  rabss2  3307  rabxmdc  3523  undif4  3554  ssdif0im  3556  inssdif0im  3559  ssundifim  3575  ralf0  3594  ralm  3595  intmin4  3951  dfiin2g  3998  invdisj  4076  trint  4197  a9evsep  4206  axnul  4209  csbexga  4212  exmidn0m  4285  exmidsssn  4286  exmidsssnc  4287  exmid0el  4288  ordunisuc2r  4606  tfi  4674  peano5  4690  ssrelrel  4819  issref  5111  iotanul  5294  iota4  5298  dffun5r  5330  fundif  5365  fv3  5652  mptfvex  5722  ssoprab2  6066  mpofvex  6357  tfri1dALT  6503  prodeq2w  12075  bj-nfalt  16152  elabgft1  16166  bj-rspgt  16174  bj-axemptylem  16279  bj-indind  16319  setindis  16354  bdsetindis  16356  bj-inf2vnlem1  16357  bj-inf2vn  16361  bj-inf2vn2  16362