Theorem alimi 1455

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

Syntax hints:   -> wi 4   A.wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-5 1447  ax-gen 1449

This theorem is referenced by:  2alimi  1456  al2imi  1458  alrimih  1469  hbal  1477  19.26  1481  19.33  1484  hbequid  1513  equidqe  1532  hbim  1545  hbor  1546  nford  1567  nfand  1568  nfal  1576  nfalt  1578  19.21ht  1581  exbi  1604  19.29  1620  19.25  1626  alexim  1645  alexnim  1648  19.9hd  1662  19.32r  1680  ax10  1717  spimh  1737  equvini  1758  nfexd  1761  stdpc4  1775  ax10oe  1797  sbcof2  1810  sb4bor  1835  nfsb2or  1837  spsbim  1843  ax16i  1858  sbi2v  1892  nfsbt  1976  nfsbd  1977  sbalyz  1999  hbsb4t  2013  dvelimor  2018  sbal2  2020  mo2n  2054  eumo0  2057  mor  2068  bm1.1  2162  alral  2522  rgen2a  2531  ralimi2  2537  rexim  2571  r19.32r  2623  ceqsalt  2764  spcgft  2815  spcegft  2817  spc2gv  2829  spc3gv  2831  rspct  2835  elabgt  2879  reu6  2927  sbciegft  2994  csbeq2  3082  csbnestgf  3110  ssrmof  3219  rabss2  3239  rabxmdc  3455  undif4  3486  ssdif0im  3488  inssdif0im  3491  ssundifim  3507  ralf0  3527  ralm  3528  intmin4  3873  dfiin2g  3920  invdisj  3998  trint  4117  a9evsep  4126  axnul  4129  csbexga  4132  exmidn0m  4202  exmidsssn  4203  exmidsssnc  4204  exmid0el  4205  ordunisuc2r  4514  tfi  4582  peano5  4598  ssrelrel  4727  issref  5012  iotanul  5194  iota4  5197  dffun5r  5229  fv3  5539  mptfvex  5602  ssoprab2  5931  mpofvex  6204  tfri1dALT  6352  prodeq2w  11564  bj-nfalt  14519  elabgft1  14533  bj-rspgt  14541  bj-axemptylem  14647  bj-indind  14687  setindis  14722  bdsetindis  14724  bj-inf2vnlem1  14725  bj-inf2vn  14729  bj-inf2vn2  14730