Theorem alimi 1479

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

Syntax hints:   -> wi 4   A.wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-5 1471  ax-gen 1473

This theorem is referenced by:  2alimi  1480  al2imi  1482  alrimih  1493  hbal  1501  19.26  1505  19.33  1508  hbequid  1537  equidqe  1556  hbim  1569  hbor  1570  nford  1591  nfand  1592  nfal  1600  nfalt  1602  19.21ht  1605  exbi  1628  19.29  1644  19.25  1650  alexim  1669  alexnim  1672  19.9hd  1686  19.32r  1704  ax10  1741  spimh  1761  equvini  1782  nfexd  1785  stdpc4  1799  ax10oe  1821  sbcof2  1834  sb4bor  1859  nfsb2or  1861  spsbim  1867  ax16i  1882  sbi2v  1917  nfsbt  2005  nfsbd  2006  sbalyz  2028  hbsb4t  2042  dvelimor  2047  sbal2  2049  mo2n  2083  eumo0  2086  mor  2098  bm1.1  2192  alral  2553  rgen2a  2562  ralimi2  2568  rexim  2602  r19.32r  2654  ceqsalt  2803  spcgft  2857  spcegft  2859  spc2gv  2871  spc3gv  2873  rspct  2877  elabgt  2921  reu6  2969  sbciegft  3036  csbeq2  3125  csbnestgf  3154  ssrmof  3264  rabss2  3284  rabxmdc  3500  undif4  3531  ssdif0im  3533  inssdif0im  3536  ssundifim  3552  ralf0  3571  ralm  3572  intmin4  3927  dfiin2g  3974  invdisj  4052  trint  4173  a9evsep  4182  axnul  4185  csbexga  4188  exmidn0m  4261  exmidsssn  4262  exmidsssnc  4263  exmid0el  4264  ordunisuc2r  4580  tfi  4648  peano5  4664  ssrelrel  4793  issref  5084  iotanul  5266  iota4  5270  dffun5r  5302  fundif  5337  fv3  5622  mptfvex  5688  ssoprab2  6024  mpofvex  6314  tfri1dALT  6460  prodeq2w  11982  bj-nfalt  15900  elabgft1  15914  bj-rspgt  15922  bj-axemptylem  16027  bj-indind  16067  setindis  16102  bdsetindis  16104  bj-inf2vnlem1  16105  bj-inf2vn  16109  bj-inf2vn2  16110