Theorem alimi 1432

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

Syntax hints:   -> wi 4   A.wal 1330

This theorem was proved from axioms:  ax-mp 5  ax-5 1424  ax-gen 1426

This theorem is referenced by:  2alimi  1433  al2imi  1435  alrimih  1446  hbal  1454  19.26  1458  19.33  1461  hbequid  1494  equidqe  1513  hbim  1525  hbor  1526  nford  1547  nfand  1548  nfalt  1558  19.21ht  1561  exbi  1584  19.29  1600  19.25  1606  alexim  1625  alexnim  1628  19.9hd  1641  19.32r  1659  ax10  1696  spimh  1716  equvini  1732  nfexd  1735  stdpc4  1749  ax10oe  1770  sbcof2  1783  sb4bor  1808  nfsb2or  1810  spsbim  1816  ax16i  1831  sbi2v  1865  nfsbt  1950  nfsbd  1951  sbalyz  1975  hbsb4t  1989  dvelimor  1994  sbal2  1998  mo2n  2028  eumo0  2031  mor  2042  bm1.1  2125  alral  2481  rgen2a  2489  ralimi2  2495  rexim  2529  r19.32r  2581  ceqsalt  2715  spcgft  2766  spcegft  2768  spc2gv  2780  spc3gv  2782  rspct  2786  elabgt  2829  reu6  2877  sbciegft  2943  csbeq2  3031  csbnestgf  3057  ssrmof  3165  rabss2  3185  rabxmdc  3399  undif4  3430  ssdif0im  3432  inssdif0im  3435  ssundifim  3451  ralf0  3471  ralm  3472  intmin4  3807  dfiin2g  3854  invdisj  3931  trint  4049  a9evsep  4058  axnul  4061  csbexga  4064  exmidn0m  4132  exmidsssn  4133  exmidsssnc  4134  exmid0el  4135  ordunisuc2r  4438  tfi  4504  peano5  4520  ssrelrel  4647  issref  4929  iotanul  5111  iota4  5114  dffun5r  5143  fv3  5452  mptfvex  5514  ssoprab2  5835  mpofvex  6109  tfri1dALT  6256  prodeq2w  11357  bj-nfalt  13142  elabgft1  13156  bj-rspgt  13164  bj-axemptylem  13261  bj-indind  13301  setindis  13336  bdsetindis  13338  bj-inf2vnlem1  13339  bj-inf2vn  13343  bj-inf2vn2  13344