Theorem alimi 1477

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

Syntax hints:   -> wi 4   A.wal 1370

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

This theorem is referenced by:  2alimi  1478  al2imi  1480  alrimih  1491  hbal  1499  19.26  1503  19.33  1506  hbequid  1535  equidqe  1554  hbim  1567  hbor  1568  nford  1589  nfand  1590  nfal  1598  nfalt  1600  19.21ht  1603  exbi  1626  19.29  1642  19.25  1648  alexim  1667  alexnim  1670  19.9hd  1684  19.32r  1702  ax10  1739  spimh  1759  equvini  1780  nfexd  1783  stdpc4  1797  ax10oe  1819  sbcof2  1832  sb4bor  1857  nfsb2or  1859  spsbim  1865  ax16i  1880  sbi2v  1915  nfsbt  2003  nfsbd  2004  sbalyz  2026  hbsb4t  2040  dvelimor  2045  sbal2  2047  mo2n  2081  eumo0  2084  mor  2095  bm1.1  2189  alral  2550  rgen2a  2559  ralimi2  2565  rexim  2599  r19.32r  2651  ceqsalt  2797  spcgft  2849  spcegft  2851  spc2gv  2863  spc3gv  2865  rspct  2869  elabgt  2913  reu6  2961  sbciegft  3028  csbeq2  3116  csbnestgf  3145  ssrmof  3255  rabss2  3275  rabxmdc  3491  undif4  3522  ssdif0im  3524  inssdif0im  3527  ssundifim  3543  ralf0  3562  ralm  3563  intmin4  3912  dfiin2g  3959  invdisj  4037  trint  4156  a9evsep  4165  axnul  4168  csbexga  4171  exmidn0m  4244  exmidsssn  4245  exmidsssnc  4246  exmid0el  4247  ordunisuc2r  4561  tfi  4629  peano5  4645  ssrelrel  4774  issref  5064  iotanul  5246  iota4  5250  dffun5r  5282  fundif  5317  fv3  5598  mptfvex  5664  ssoprab2  6000  mpofvex  6290  tfri1dALT  6436  prodeq2w  11838  bj-nfalt  15662  elabgft1  15676  bj-rspgt  15684  bj-axemptylem  15790  bj-indind  15830  setindis  15865  bdsetindis  15867  bj-inf2vnlem1  15868  bj-inf2vn  15872  bj-inf2vn2  15873