Theorem alimi 1503

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 1495	. 2 |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
2		alimi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1499	1 |- ( A. x ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1395

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

This theorem is referenced by:  2alimi  1504  al2imi  1506  alrimih  1517  hbal  1525  19.26  1529  19.33  1532  hbequid  1561  equidqe  1580  hbim  1593  hbor  1594  nford  1615  nfand  1616  nfal  1624  nfalt  1626  19.21ht  1629  exbi  1652  19.29  1668  19.25  1674  alexim  1693  alexnim  1696  19.9hd  1710  19.32r  1728  ax10  1765  spimh  1785  equvini  1806  nfexd  1809  stdpc4  1823  ax10oe  1845  sbcof2  1858  sb4bor  1883  nfsb2or  1885  spsbim  1891  ax16i  1906  sbi2v  1941  nfsbt  2029  nfsbd  2030  sbalyz  2052  hbsb4t  2066  dvelimor  2071  sbal2  2073  mo2n  2107  eumo0  2110  mor  2122  bm1.1  2216  alral  2577  rgen2a  2586  ralimi2  2592  rexim  2626  r19.32r  2679  ceqsalt  2829  spcgft  2883  spcegft  2885  spc2gv  2897  spc3gv  2899  rspct  2903  elabgt  2947  reu6  2995  sbciegft  3062  csbeq2  3151  csbnestgf  3180  ssrmof  3290  rabss2  3310  rabxmdc  3526  undif4  3557  ssdif0im  3559  inssdif0im  3562  ssundifim  3578  ralf0  3597  ralm  3598  intmin4  3956  dfiin2g  4003  invdisj  4081  trint  4202  a9evsep  4211  axnul  4214  csbexga  4217  exmidn0m  4291  exmidsssn  4292  exmidsssnc  4293  exmid0el  4294  ordunisuc2r  4612  tfi  4680  peano5  4696  ssrelrel  4826  issref  5119  iotanul  5302  iota4  5306  dffun5r  5338  fundif  5374  fv3  5662  mptfvex  5732  ssoprab2  6076  mpofvex  6369  tfri1dALT  6516  prodeq2w  12116  bj-nfalt  16360  elabgft1  16374  bj-rspgt  16382  bj-axemptylem  16487  bj-indind  16527  setindis  16562  bdsetindis  16564  bj-inf2vnlem1  16565  bj-inf2vn  16569  bj-inf2vn2  16570