Theorem a4s 984

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 973	. 2 |- (A.xph -> ph)
2		a4s.1	. 2 |- (ph -> ps)
3	1, 2	syl 10	1 |- (A.xph -> ps)

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  19.20i 992  19.2 1030  19.21t 1115  exintr 1117  ax10o 1139  cbv1 1162  equvini 1168  drsb1 1175  sbied 1195  ax11v2 1215  dfsb2 1225  sbequi 1228  drsb2 1230  sbn 1231  sbi1 1232  hbsb4 1248  hbsb4t 1249  sbidm 1254  sbco2 1255  sbcom 1258  sbcom2 1334  sbal1 1346  ax11eq 1363  ax11el 1364  ax11inda 1371  a12lem1 1376  mopick 1433  rgen2a 1698  ralcom2 1775  reu3 1929  sbcralt 1988  sbcrext 1989  sbcralgf 1990  sbcrexgf 1991  csbie2t 2031  csbnestg 2034  sbcnestg 2036  moabex 2764  mosubopt 2802  ssopab2 2820  dfid3 2834  alxfr 2894  dmcosseq 3363  fununi 3561  fv3 3731  cbvfo 3883  fnoprabg 4010  pssnn 4527  kmlem16 4768  axextnd 4931  axrepndlem1 4932  axrepndlem2 4933  axunndlem1 4935  axunnd 4936  axpowndlem1 4937  axpowndlem2 4938  axpowndlem3 4939  axpowndlem4 4940  axregndlem1 4942  axregndlem2 4943  axregnd 4944  axinfndlem1 4945  axinfnd 4946  axacndlem4 4950  axacndlem5 4951  axacnd 4952  suppsr3 5212  uninqs 10396  cmphmp 10463  qusp 10485  imonclem 10651

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

Copyright terms: Public domain