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 )

This proof depends on syntax axioms:   -> wi 4   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-5 1500  ax-gen 1502

This theorem is used 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  3587  ssdif0im  3589  inssdif0imOLD  3593  ssundifim  3611  ralf0  3630  ralm  3631  intmin4  3998  dfiin2g  4045  invdisj  4123  trint  4244  a9evsep  4255  axnul  4258  csbexga  4261  exmidn0m  4338  exmidsssn  4339  exmidsssnc  4340  exmid0el  4341  ordunisuc2r  4661  tfi  4729  peano5  4745  ssrelrel  4875  issref  5170  iotanul  5353  iota4  5357  dffun5r  5389  fundif  5425  fv3  5718  mptfvex  5791  ssoprab2  6144  mpofvex  6441  tfri1dALT  6622  prodeq2w  12323  bj-nfalt  16792  elabgft1  16806  bj-rspgt  16814  bj-axemptylem  16918  bj-indind  16958  setindis  16993  bdsetindis  16995  bj-inf2vnlem1  16996  bj-inf2vn  17000  bj-inf2vn2  17001  als-no-surprise  17147