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  2672  rgen2a  2680  ralimi2  2686  ceqsalt  2881  spcgft  2931  rspct  2948  elabgt  2982  reu6  3025  sbciegft  3076  csbexg  3146  csbnestgf  3184  rabss2  3349  undif4  3607  ralf0  3656  intmin4  3955  dfiin2g  4000  iotanul  4354  iota4  4357  peano2  4403  nnsucelr  4428  fv3  5341  clos1nrel  5886