Theorem alimi 1478

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

Syntax hints:   -> wi 4   A.wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-5 1470  ax-gen 1472

This theorem is referenced by:  2alimi  1479  al2imi  1481  alrimih  1492  hbal  1500  19.26  1504  19.33  1507  hbequid  1536  equidqe  1555  hbim  1568  hbor  1569  nford  1590  nfand  1591  nfal  1599  nfalt  1601  19.21ht  1604  exbi  1627  19.29  1643  19.25  1649  alexim  1668  alexnim  1671  19.9hd  1685  19.32r  1703  ax10  1740  spimh  1760  equvini  1781  nfexd  1784  stdpc4  1798  ax10oe  1820  sbcof2  1833  sb4bor  1858  nfsb2or  1860  spsbim  1866  ax16i  1881  sbi2v  1916  nfsbt  2004  nfsbd  2005  sbalyz  2027  hbsb4t  2041  dvelimor  2046  sbal2  2048  mo2n  2082  eumo0  2085  mor  2096  bm1.1  2190  alral  2551  rgen2a  2560  ralimi2  2566  rexim  2600  r19.32r  2652  ceqsalt  2798  spcgft  2850  spcegft  2852  spc2gv  2864  spc3gv  2866  rspct  2870  elabgt  2914  reu6  2962  sbciegft  3029  csbeq2  3117  csbnestgf  3146  ssrmof  3256  rabss2  3276  rabxmdc  3492  undif4  3523  ssdif0im  3525  inssdif0im  3528  ssundifim  3544  ralf0  3563  ralm  3564  intmin4  3913  dfiin2g  3960  invdisj  4038  trint  4157  a9evsep  4166  axnul  4169  csbexga  4172  exmidn0m  4245  exmidsssn  4246  exmidsssnc  4247  exmid0el  4248  ordunisuc2r  4562  tfi  4630  peano5  4646  ssrelrel  4775  issref  5065  iotanul  5247  iota4  5251  dffun5r  5283  fundif  5318  fv3  5599  mptfvex  5665  ssoprab2  6001  mpofvex  6291  tfri1dALT  6437  prodeq2w  11867  bj-nfalt  15700  elabgft1  15714  bj-rspgt  15722  bj-axemptylem  15828  bj-indind  15868  setindis  15903  bdsetindis  15905  bj-inf2vnlem1  15906  bj-inf2vn  15910  bj-inf2vn2  15911