Theorem alimi 1384

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

Syntax hints:   -> wi 4   A.wal 1282

This theorem was proved from axioms:  ax-mp 7  ax-5 1376  ax-gen 1378

This theorem is referenced by:  2alimi  1385  al2imi  1387  alrimih  1398  hbal  1406  19.26  1410  19.33  1413  hbequid  1446  equidqe  1465  hbim  1477  hbor  1478  nford  1499  nfand  1500  nfalt  1510  19.21ht  1513  exbi  1535  19.29  1551  19.25  1557  alexim  1576  alexnim  1579  19.9hd  1592  19.32r  1610  ax10  1645  spimh  1665  equvini  1681  nfexd  1684  stdpc4  1698  ax10oe  1718  sbcof2  1731  sb4bor  1756  nfsb2or  1758  spsbim  1764  ax16i  1779  sbi2v  1813  nfsbt  1891  nfsbd  1892  sbalyz  1916  hbsb4t  1930  dvelimor  1935  sbal2  1939  mo2n  1969  eumo0  1972  mor  1983  bm1.1  2066  alral  2409  rgen2a  2417  ralimi2  2423  rexim  2455  r19.32r  2501  ceqsalt  2625  spcgft  2675  spcegft  2677  spc2gv  2688  spc3gv  2690  rspct  2694  elabgt  2735  reu6  2781  sbciegft  2844  csbnestgf  2954  rabss2  3077  rabxmdc  3276  undif4  3306  ssdif0im  3308  inssdif0im  3311  ssundifim  3326  ralf0  3344  ralm  3345  intmin4  3664  dfiin2g  3711  invdisj  3780  trint  3890  a9evsep  3900  axnul  3903  csbexga  3906  ordunisuc2r  4258  tfi  4323  peano5  4339  ssrelrel  4458  issref  4727  iotanul  4902  iota4  4905  dffun5r  4934  fv3  5218  mptfvex  5277  ssoprab2  5581  mpt2fvex  5849  bj-nfalt  10575  elabgft1  10588  bj-rspgt  10596  bj-axemptylem  10683  bj-indind  10727  setindis  10762  bdsetindis  10764  bj-inf2vnlem1  10765  bj-inf2vn  10769  bj-inf2vn2  10770