Theorem alimi 1390

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

Syntax hints:   -> wi 4   A.wal 1288

This theorem was proved from axioms:  ax-mp 7  ax-5 1382  ax-gen 1384

This theorem is referenced by:  2alimi  1391  al2imi  1393  alrimih  1404  hbal  1412  19.26  1416  19.33  1419  hbequid  1452  equidqe  1471  hbim  1483  hbor  1484  nford  1505  nfand  1506  nfalt  1516  19.21ht  1519  exbi  1541  19.29  1557  19.25  1563  alexim  1582  alexnim  1585  19.9hd  1598  19.32r  1616  ax10  1653  spimh  1673  equvini  1689  nfexd  1692  stdpc4  1706  ax10oe  1726  sbcof2  1739  sb4bor  1764  nfsb2or  1766  spsbim  1772  ax16i  1787  sbi2v  1821  nfsbt  1899  nfsbd  1900  sbalyz  1924  hbsb4t  1938  dvelimor  1943  sbal2  1947  mo2n  1977  eumo0  1980  mor  1991  bm1.1  2074  alral  2422  rgen2a  2430  ralimi2  2436  rexim  2468  r19.32r  2515  ceqsalt  2646  spcgft  2697  spcegft  2699  spc2gv  2710  spc3gv  2712  rspct  2716  elabgt  2758  reu6  2805  sbciegft  2870  csbnestgf  2981  rabss2  3105  rabxmdc  3318  undif4  3349  ssdif0im  3351  inssdif0im  3354  ssundifim  3370  ralf0  3389  ralm  3390  intmin4  3722  dfiin2g  3769  invdisj  3845  trint  3957  a9evsep  3967  axnul  3970  csbexga  3973  exmidn0m  4039  exmidsssn  4040  exmid0el  4041  ordunisuc2r  4344  tfi  4410  peano5  4426  ssrelrel  4551  issref  4827  iotanul  5008  iota4  5011  dffun5r  5040  fv3  5341  mptfvex  5401  ssoprab2  5719  mpt2fvex  5987  tfri1dALT  6130  bj-nfalt  11931  elabgft1  11944  bj-rspgt  11952  bj-axemptylem  12049  bj-indind  12093  setindis  12128  bdsetindis  12130  bj-inf2vnlem1  12131  bj-inf2vn  12135  bj-inf2vn2  12136