Theorem a4s 1619

Description: Generalization of antecedent.

Hypothesis

Ref	Expression
a4s.1	|- (ph -> ps)

Assertion

Ref	Expression
a4s	|- (A.xph -> ps)

Proof of Theorem a4s

Step	Hyp	Ref	Expression
1		ax-4 1608	. 2 |- (A.xph -> ph)
2		a4s.1	. 2 |- (ph -> ps)
3	1, 2	syl 13	1 |- (A.xph -> ps)

Syntax hints:   -> wi 3  A.wal 1584

This theorem is referenced by:  alimi 1627  19.2 1666  19.21t 1755  exintr 1757  ax10o 1780  cbv1 1804  equveli 1812  drsb1 1819  ax11v2 1861  dfsb2 1871  sbequi 1874  drsb2 1876  sbn 1877  sbi1 1878  sbf3t 1894  hbsb4 1895  hbsb4t 1896  sbco2 1902  sbcom 1905  sbcom2 1990  sbal1 2001  ax11eq 2018  ax11el 2019  ax11inda 2026  a12lem1 2031  eujustALT 2040  mopick 2094  eupickbi 2098  ralcom2 2490  ceqsalg 2562  cla4gft 2601  reu6 2689  sbcralt 2759  sbcrext 2760  sbcralgf 2761  sbcrexgf 2762  csbie2t 2809  csbnestg 2812  sbcnestg 2814  reldisj 3121  moabex 3676  mosubopt 3714  ssopab2 3734  dfid3 3748  alxfr 3982  fununi 4582  fv3 4779  cbvfo 4956  fnoprabg 5034  pssnn 5834  kmlem16 6352  axextnd 6461  axrepndlem1 6462  axrepndlem2 6463  axunndlem1 6465  axunnd 6466  axpowndlem1 6467  axpowndlem2 6468  axpowndlem3 6469  axpowndlem4 6470  axregndlem1 6472  axregndlem2 6473  axregnd 6474  axinfndlem1 6475  axinfnd 6476  axacndlem4 6480  axacndlem5 6481  axacnd 6482  suppsr3 6742  bnj9 13175  fundmpss 14467  wfrlem5 14614  frrlem5 14638  nalf 14853  uninqs 15048  ref4w 15080  pospos 15374  cmphmp 15635  qusp 15671  bwt2 15738  imonclem 15956  pm10.55 17140  2albi 17154  pm11.57 17170  ax4567to6 17186  ax10ext 17188  ax10-16 17189  pm14.122b 17211  pm14.123b 17214  eupickbiOLD 17224  cla4gftOLD 17230  dropab1 17248  dropab2 17249

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-4 1608

Copyright terms: Public domain