Theorem alimi 1431

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

Syntax hints:   -> wi 4   A.wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-5 1423  ax-gen 1425

This theorem is referenced by:  2alimi  1432  al2imi  1434  alrimih  1445  hbal  1453  19.26  1457  19.33  1460  hbequid  1493  equidqe  1512  hbim  1524  hbor  1525  nford  1546  nfand  1547  nfalt  1557  19.21ht  1560  exbi  1583  19.29  1599  19.25  1605  alexim  1624  alexnim  1627  19.9hd  1640  19.32r  1658  ax10  1695  spimh  1715  equvini  1731  nfexd  1734  stdpc4  1748  ax10oe  1769  sbcof2  1782  sb4bor  1807  nfsb2or  1809  spsbim  1815  ax16i  1830  sbi2v  1864  nfsbt  1949  nfsbd  1950  sbalyz  1974  hbsb4t  1988  dvelimor  1993  sbal2  1997  mo2n  2027  eumo0  2030  mor  2041  bm1.1  2124  alral  2478  rgen2a  2486  ralimi2  2492  rexim  2526  r19.32r  2578  ceqsalt  2712  spcgft  2763  spcegft  2765  spc2gv  2776  spc3gv  2778  rspct  2782  elabgt  2825  reu6  2873  sbciegft  2939  csbeq2  3026  csbnestgf  3052  ssrmof  3160  rabss2  3180  rabxmdc  3394  undif4  3425  ssdif0im  3427  inssdif0im  3430  ssundifim  3446  ralf0  3466  ralm  3467  intmin4  3799  dfiin2g  3846  invdisj  3923  trint  4041  a9evsep  4050  axnul  4053  csbexga  4056  exmidn0m  4124  exmidsssn  4125  exmidsssnc  4126  exmid0el  4127  ordunisuc2r  4430  tfi  4496  peano5  4512  ssrelrel  4639  issref  4921  iotanul  5103  iota4  5106  dffun5r  5135  fv3  5444  mptfvex  5506  ssoprab2  5827  mpofvex  6101  tfri1dALT  6248  prodeq2w  11325  bj-nfalt  12971  elabgft1  12985  bj-rspgt  12993  bj-axemptylem  13090  bj-indind  13130  setindis  13165  bdsetindis  13167  bj-inf2vnlem1  13168  bj-inf2vn  13172  bj-inf2vn2  13173