Theorem a4s 981

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

This theorem is referenced by:  19.20i 989  19.2 1026  19.21t 1111  exintr 1113  ax10o 1135  cbv1 1158  equvini 1164  drsb1 1171  sbied 1191  ax11v2 1210  dfsb2 1220  sbequi 1223  drsb2 1225  sbn 1226  sbi1 1227  hbsb4 1243  hbsb4t 1244  sbidm 1249  sbco2 1250  sbcom 1253  sbcom2 1329  sbal1 1341  ax11eq 1356  ax11el 1357  ax11inda 1364  a12lem1 1369  mopick 1426  rgen2a 1691  ralcom2 1768  reu3 1921  sbcralt 1980  sbcrext 1981  sbcralgf 1982  sbcrexgf 1983  csbie2t 2023  csbnestg 2026  sbcnestg 2028  moabex 2756  mosubopt 2793  ssopab2 2811  dfid3 2826  alxfr 2886  dmcosseq 3349  fununi 3549  fv3 3718  cbvfo 3870  fnoprabg 3997  pssnn 4513  kmlem16 4752  axextnd 4915  axrepndlem1 4916  axrepndlem2 4917  axunndlem1 4919  axunnd 4920  axpowndlem1 4921  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axregndlem1 4926  axregndlem2 4927  axregnd 4928  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936  suppsr3 5196  uninqs 10342  cmphmp 10408  qusp 10430  imonclem 10583

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

Copyright terms: Public domain