Theorem alimi 1559

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 1557	. 2 |- (A.x(ph -> ps) -> (A.xph -> A.xps))
2		alimi.1	. 2 |- (ph -> ps)
3	1, 2	mpg 1548	1 |- (A.xph -> A.xps)

Syntax hints:   -> wi 4  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-gen 1546  ax-5 1557

This theorem is referenced by:  2alimi  1560  al2imi  1561  alrimih  1565  exbi  1581  19.26  1593  19.29  1596  19.25  1603  19.33  1607  equidOLD  1677  alcomiw  1704  hbn1fw  1705  hba1w  1707  hbalw  1709  ax11dgen  1722  hbal  1736  ax5o  1749  hba1OLD  1787  19.38  1794  nfimdOLD  1809  hbimdOLD  1816  dvelimhw  1849  cbv3hv  1850  cbv3hvOLD  1851  19.21tOLD  1863  dvelimv  1939  ax10  1944  equvini  1987  stdpc4  2024  ax16i  2046  sbco3  2088  sb9i  2094  sbal1  2126  hba1-o  2149  aecom-o  2151  ax11  2155  hbequid  2160  ax67  2165  ax67to6  2167  ax67to7  2168  ax467  2169  ax467to6  2171  ax467to7  2172  equidqe  2173  equid1ALT  2176  ax10from10o  2177  ax10-16  2190  ax11eq  2193  ax11el  2194  ax11indi  2196  mo  2226  eumo0  2228  mo2  2233  2mo  2282  axi5r  2326  bm1.1  2338  alral  2673  rgen2a  2681  ralimi2  2687  ceqsalt  2882  spcgft  2932  rspct  2949  elabgt  2983  reu6  3026  sbciegft  3077  csbexg  3147  csbnestgf  3185  rabss2  3350  undif4  3608  ralf0  3657  intmin4  3956  dfiin2g  4001  iotanul  4355  iota4  4358  peano2  4404  nnsucelr  4429  fv3  5342  clos1nrel  5887