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  3950  dfiin2g  3997  invdisj  4075  trint  4196  a9evsep  4205  axnul  4208  csbexga  4211  exmidn0m  4284  exmidsssn  4285  exmidsssnc  4286  exmid0el  4287  ordunisuc2r  4603  tfi  4671  peano5  4687  ssrelrel  4816  issref  5107  iotanul  5290  iota4  5294  dffun5r  5326  fundif  5361  fv3  5646  mptfvex  5713  ssoprab2  6051  mpofvex  6341  tfri1dALT  6487  prodeq2w  12053  bj-nfalt  16058  elabgft1  16072  bj-rspgt  16080  bj-axemptylem  16185  bj-indind  16225  setindis  16260  bdsetindis  16262  bj-inf2vnlem1  16263  bj-inf2vn  16267  bj-inf2vn2  16268