Theorem alimi 1508

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

Syntax hints:   -> wi 4   A.wal 1400

This theorem was proved from axioms:  ax-mp 5  ax-5 1500  ax-gen 1502

This theorem is referenced by:  2alimi  1509  al2imi  1511  alrimih  1522  hbal  1530  19.26  1534  19.33  1537  hbequid  1566  equidqe  1585  hbim  1598  hbor  1599  nford  1620  nfand  1621  nfal  1629  nfalt  1631  19.21ht  1634  exbi  1657  19.29  1673  19.25  1679  alexim  1698  alexnim  1701  19.9hd  1714  19.32r  1732  ax10  1769  spimh  1790  equvini  1811  nfexd  1814  stdpc4  1828  ax10oe  1850  sbcof2  1863  sb4bor  1888  nfsb2or  1890  spsbim  1896  ax16i  1911  sbi2v  1947  nfsbt  2036  nfsbd  2037  sbalyz  2059  hbsb4t  2073  dvelimor  2078  sbal2  2080  mo2n  2114  eumo0  2117  mor  2129  bm1.1  2223  alral  2595  rgen2a  2604  ralimi2  2610  rexim  2644  r19.32r  2697  ceqsalt  2848  spcgft  2902  spcegft  2904  spc2gv  2916  spc3gv  2918  rspct  2922  elabgt  2967  reu6  3015  sbciegft  3082  csbeq2  3171  csbnestgf  3200  ssrmof  3311  rabss2  3331  undif4  3586  ssdif0im  3588  inssdif0im  3591  ssundifim  3608  ralf0  3627  ralm  3628  intmin4  3993  dfiin2g  4040  invdisj  4118  trint  4239  a9evsep  4250  axnul  4253  csbexga  4256  exmidn0m  4333  exmidsssn  4334  exmidsssnc  4335  exmid0el  4336  ordunisuc2r  4656  tfi  4724  peano5  4740  ssrelrel  4870  issref  5165  iotanul  5348  iota4  5352  dffun5r  5384  fundif  5420  fv3  5713  mptfvex  5785  ssoprab2  6134  mpofvex  6431  tfri1dALT  6612  prodeq2w  12301  bj-nfalt  16706  elabgft1  16720  bj-rspgt  16728  bj-axemptylem  16832  bj-indind  16872  setindis  16907  bdsetindis  16909  bj-inf2vnlem1  16910  bj-inf2vn  16914  bj-inf2vn2  16915