Theorem alimi 1501

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
alimi.1	|- ( ph -> ps )

Assertion

Ref	Expression
alimi	|- ( A. x ph -> A. x ps )

Proof of Theorem alimi

Step	Hyp	Ref	Expression
1		ax-5 1493	. 2 |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
2		alimi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1497	1 |- ( A. x ph -> A. x ps )

Syntax hints:   -> wi 4   A.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  4605  tfi  4673  peano5  4689  ssrelrel  4818  issref  5110  iotanul  5293  iota4  5297  dffun5r  5329  fundif  5364  fv3  5649  mptfvex  5719  ssoprab2  6059  mpofvex  6349  tfri1dALT  6495  prodeq2w  12062  bj-nfalt  16086  elabgft1  16100  bj-rspgt  16108  bj-axemptylem  16213  bj-indind  16253  setindis  16288  bdsetindis  16290  bj-inf2vnlem1  16291  bj-inf2vn  16295  bj-inf2vn2  16296