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  2827  spcgft  2881  spcegft  2883  spc2gv  2895  spc3gv  2897  rspct  2901  elabgt  2945  reu6  2993  sbciegft  3060  csbeq2  3149  csbnestgf  3178  ssrmof  3288  rabss2  3308  rabxmdc  3524  undif4  3555  ssdif0im  3557  inssdif0im  3560  ssundifim  3576  ralf0  3595  ralm  3596  intmin4  3954  dfiin2g  4001  invdisj  4079  trint  4200  a9evsep  4209  axnul  4212  csbexga  4215  exmidn0m  4289  exmidsssn  4290  exmidsssnc  4291  exmid0el  4292  ordunisuc2r  4610  tfi  4678  peano5  4694  ssrelrel  4824  issref  5117  iotanul  5300  iota4  5304  dffun5r  5336  fundif  5371  fv3  5658  mptfvex  5728  ssoprab2  6072  mpofvex  6365  tfri1dALT  6512  prodeq2w  12107  bj-nfalt  16296  elabgft1  16310  bj-rspgt  16318  bj-axemptylem  16423  bj-indind  16463  setindis  16498  bdsetindis  16500  bj-inf2vnlem1  16501  bj-inf2vn  16505  bj-inf2vn2  16506