Theorem a4s 960

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 951	. 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 950

This theorem is referenced by:  19.20i 968  19.2 1006  19.21t 1091  exintr 1093  cbv1 1145  equvini 1151  drsb1 1158  sbied 1178  ax11v2 1199  dfsb2 1209  sbequi 1212  drsb2 1214  sbn 1215  sbi1 1216  hbsb4 1232  hbsb4t 1233  sbidm 1238  sbco2 1239  sbcom 1242  sbcom2 1316  sbal1 1328  ax11eq 1340  ax11el 1341  ax11inda 1348  a12lem1 1353  mopick 1410  rgen2a 1675  ralcom2 1752  reu3 1902  sbcralt 1961  sbcrext 1962  sbcralgf 1963  sbcrexgf 1964  csbie2t 2004  csbnestg 2007  sbcnestg 2009  moabex 2734  mosubopt 2767  ssopab2 2784  dfid3 2799  alxfr 2859  dmcosseq 3316  fununi 3503  fv3 3672  cbvfo 3824  fnoprabg 3951  pssnn 4465  kmlem16 4704  axextnd 4866  axrepndlem1 4867  axrepndlem2 4868  axunndlem1 4870  axunnd 4871  axpowndlem1 4872  axpowndlem2 4873  axpowndlem3 4874  axpowndlem4 4875  axregndlem1 4877  axregndlem2 4878  axregnd 4879  axinfndlem1 4880  axinfnd 4881  axacndlem4 4885  axacndlem5 4886  axacnd 4887  suppsr3 5147  uninqs 8701  cmphmp 8759  qusp 8780  imonclem 8933

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

Copyright terms: Public domain