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  4286  exmidsssn  4287  exmidsssnc  4288  exmid0el  4289  ordunisuc2r  4607  tfi  4675  peano5  4691  ssrelrel  4821  issref  5114  iotanul  5297  iota4  5301  dffun5r  5333  fundif  5368  fv3  5655  mptfvex  5725  ssoprab2  6069  mpofvex  6362  tfri1dALT  6508  prodeq2w  12088  bj-nfalt  16237  elabgft1  16251  bj-rspgt  16259  bj-axemptylem  16364  bj-indind  16404  setindis  16439  bdsetindis  16441  bj-inf2vnlem1  16442  bj-inf2vn  16446  bj-inf2vn2  16447