Theorem alimi 1341

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.xph -> A.xps)

Proof of Theorem alimi

Step	Hyp	Ref	Expression
1		ax-5 1333	. 2 |- (A.x(ph -> ps) -> (A.xph -> A.xps))
2		alimi.1	. 2 |- (ph -> ps)
3	1, 2	mpg 1337	1 |- (A.xph -> A.xps)

Syntax hints:   -> wi 4  A.wal 1240

This theorem was proved from axioms:  ax-mp 7  ax-5 1333  ax-gen 1335

This theorem is referenced by:  2alimi  1342  al2imi  1344  alrimih  1355  hbal  1363  19.26  1367  19.33  1370  hbequid  1403  equidqe  1422  hbim  1434  hbor  1435  nford  1456  nfand  1457  nfalt  1467  19.21ht  1470  exbi  1492  19.29  1508  19.25  1514  alexim  1533  alexnim  1536  19.9hd  1549  19.32r  1567  ax10  1602  spimh  1622  equvini  1638  nfexd  1641  stdpc4  1655  ax10oe  1675  sbcof2  1688  sb4bor  1713  nfsb2or  1715  spsbim  1721  ax16i  1735  sbi2v  1769  nfsbt  1847  nfsbd  1848  sbalyz  1872  hbsb4t  1886  dvelimor  1891  sbal2  1895  mo2n  1925  eumo0  1928  mor  1939  bm1.1  2022  alral  2361  rgen2a  2369  ralimi2  2375  rexim  2407  r19.32r  2451  ceqsalt  2574  spcgft  2624  spcegft  2626  spc2gv  2637  spc3gv  2639  rspct  2643  elabgt  2678  reu6  2724  sbciegft  2787  csbnestgf  2892  rabss2  3017  rabxmdc  3243  undif4  3278  ssdif0im  3280  inssdif0im  3285  ssundifim  3300  ralf0  3318  ralm  3319  intmin4  3634  dfiin2g  3681  invdisj  3750  trint  3860  a9evsep  3870  axnul  3873  csbexga  3876  ordunisuc2r  4205  tfi  4248  peano5  4264  ssrelrel  4383  issref  4650  iotanul  4825  iota4  4828  dffun5r  4857  fv3  5140  mptfvex  5199  ssoprab2  5503  mpt2fvex  5771  bj-nfalt  9239  elabgft1  9252  bj-rspgt  9260  bj-axemptylem  9347  bj-indind  9391  peano5setOLD  9400  setindis  9427  bdsetindis  9429  bj-inf2vnlem1  9430  bj-inf2vn  9434  bj-inf2vn2  9435