Theorem a4s 1025

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 1014	. 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 995

This theorem is referenced by:  19.20i 1033  19.2 1071  19.21t 1156  exintr 1158  ax10o 1181  cbv1 1204  equvini 1210  drsb1 1217  sbied 1237  ax11v2 1257  dfsb2 1267  sbequi 1270  drsb2 1272  sbn 1273  sbi1 1274  hbsb4 1290  hbsb4t 1291  sbidm 1296  sbco2 1297  sbcom 1300  sbcom2 1376  sbal1 1388  ax11eq 1405  ax11el 1406  ax11inda 1413  a12lem1 1418  mopick 1475  rgen2a 1746  ralcom2 1823  reu3 1978  sbcralt 2040  sbcrext 2041  sbcralgf 2042  sbcrexgf 2043  csbie2t 2084  csbnestg 2087  sbcnestg 2089  moabex 2822  mosubopt 2860  ssopab2 2878  dfid3 2892  alxfr 2953  dmcosseq 3422  fununi 3620  fv3 3790  cbvfo 3943  fnoprabg 4070  pssnn 4599  kmlem16 4842  axextnd 5008  axrepndlem1 5009  axrepndlem2 5010  axunndlem1 5012  axunnd 5013  axpowndlem1 5014  axpowndlem2 5015  axpowndlem3 5016  axpowndlem4 5017  axregndlem1 5019  axregndlem2 5020  axregnd 5021  axinfndlem1 5022  axinfnd 5023  axacndlem4 5027  axacndlem5 5028  axacnd 5029  suppsr3 5289  uninqs 10527  ref3w 10566  cmphmp 10615  qusp 10649  imonclem 10823

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

Copyright terms: Public domain