Theorem alimi 1504

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

Syntax hints:   -> wi 4   A.wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-5 1496  ax-gen 1498

This theorem is referenced by:  2alimi  1505  al2imi  1507  alrimih  1518  hbal  1526  19.26  1530  19.33  1533  hbequid  1562  equidqe  1581  hbim  1594  hbor  1595  nford  1616  nfand  1617  nfal  1625  nfalt  1627  19.21ht  1630  exbi  1653  19.29  1669  19.25  1675  alexim  1694  alexnim  1697  19.9hd  1710  19.32r  1728  ax10  1765  spimh  1786  equvini  1807  nfexd  1810  stdpc4  1824  ax10oe  1846  sbcof2  1859  sb4bor  1884  nfsb2or  1886  spsbim  1892  ax16i  1907  sbi2v  1942  nfsbt  2030  nfsbd  2031  sbalyz  2053  hbsb4t  2067  dvelimor  2072  sbal2  2074  mo2n  2108  eumo0  2111  mor  2123  bm1.1  2217  alral  2587  rgen2a  2596  ralimi2  2602  rexim  2636  r19.32r  2689  ceqsalt  2840  spcgft  2894  spcegft  2896  spc2gv  2908  spc3gv  2910  rspct  2914  elabgt  2958  reu6  3006  sbciegft  3073  csbeq2  3162  csbnestgf  3191  ssrmof  3301  rabss2  3321  rabxmdc  3540  undif4  3571  ssdif0im  3573  inssdif0im  3576  ssundifim  3593  ralf0  3612  ralm  3613  intmin4  3977  dfiin2g  4024  invdisj  4102  trint  4223  a9evsep  4232  axnul  4235  csbexga  4238  exmidn0m  4314  exmidsssn  4315  exmidsssnc  4316  exmid0el  4317  ordunisuc2r  4636  tfi  4704  peano5  4720  ssrelrel  4850  issref  5145  iotanul  5328  iota4  5332  dffun5r  5364  fundif  5400  fv3  5693  mptfvex  5763  ssoprab2  6109  mpofvex  6401  tfri1dALT  6582  prodeq2w  12242  bj-nfalt  16536  elabgft1  16550  bj-rspgt  16558  bj-axemptylem  16662  bj-indind  16702  setindis  16737  bdsetindis  16739  bj-inf2vnlem1  16740  bj-inf2vn  16744  bj-inf2vn2  16745