Theorem alimi 1435

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

Syntax hints:   -> wi 4   A.wal 1333

This theorem was proved from axioms:  ax-mp 5  ax-5 1427  ax-gen 1429

This theorem is referenced by:  2alimi  1436  al2imi  1438  alrimih  1449  hbal  1457  19.26  1461  19.33  1464  hbequid  1493  equidqe  1512  hbim  1525  hbor  1526  nford  1547  nfand  1548  nfal  1556  nfalt  1558  19.21ht  1561  exbi  1584  19.29  1600  19.25  1606  alexim  1625  alexnim  1628  19.9hd  1642  19.32r  1660  ax10  1697  spimh  1717  equvini  1738  nfexd  1741  stdpc4  1755  ax10oe  1777  sbcof2  1790  sb4bor  1815  nfsb2or  1817  spsbim  1823  ax16i  1838  sbi2v  1872  nfsbt  1956  nfsbd  1957  sbalyz  1979  hbsb4t  1993  dvelimor  1998  sbal2  2000  mo2n  2034  eumo0  2037  mor  2048  bm1.1  2142  alral  2502  rgen2a  2511  ralimi2  2517  rexim  2551  r19.32r  2603  ceqsalt  2738  spcgft  2789  spcegft  2791  spc2gv  2803  spc3gv  2805  rspct  2809  elabgt  2853  reu6  2901  sbciegft  2967  csbeq2  3055  csbnestgf  3083  ssrmof  3191  rabss2  3211  rabxmdc  3425  undif4  3456  ssdif0im  3458  inssdif0im  3461  ssundifim  3477  ralf0  3497  ralm  3498  intmin4  3835  dfiin2g  3882  invdisj  3959  trint  4077  a9evsep  4086  axnul  4089  csbexga  4092  exmidn0m  4162  exmidsssn  4163  exmidsssnc  4164  exmid0el  4165  ordunisuc2r  4473  tfi  4541  peano5  4557  ssrelrel  4686  issref  4968  iotanul  5150  iota4  5153  dffun5r  5182  fv3  5491  mptfvex  5553  ssoprab2  5877  mpofvex  6151  tfri1dALT  6298  prodeq2w  11453  bj-nfalt  13349  elabgft1  13363  bj-rspgt  13371  bj-axemptylem  13478  bj-indind  13518  setindis  13553  bdsetindis  13555  bj-inf2vnlem1  13556  bj-inf2vn  13560  bj-inf2vn2  13561