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  4246  a9evsep  4257  axnul  4260  csbexga  4263  exmidn0m  4340  exmidsssn  4341  exmidsssnc  4342  exmid0el  4343  ordunisuc2r  4663  tfi  4731  peano5  4747  ssrelrel  4877  issref  5173  iotanul  5356  iota4  5360  dffun5r  5392  fundif  5428  fv3  5721  mptfvex  5794  ssoprab2  6147  mpofvex  6445  tfri1dALT  6626  prodeq2w  12348  bj-nfalt  16997  elabgft1  17011  bj-rspgt  17019  bj-axemptylem  17123  bj-indind  17163  setindis  17198  bdsetindis  17200  bj-inf2vnlem1  17201  bj-inf2vn  17205  bj-inf2vn2  17206  als-no-surprise  17354