Theorem a4s 1330

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

Syntax hints:   -> wi 3  A.wal 1296

This theorem is referenced by:  alimi 1338  19.2 1377  19.21t 1473  exintr 1475  ax10o 1499  cbv1 1523  equviniOLD 1532  drsb1 1539  ax11v2 1585  dfsb2 1595  sbequi 1598  drsb2 1600  sbn 1601  sbi1 1602  sbf3t 1619  hbsb4 1620  hbsb4t 1621  hbsb4tOLD 1622  sbidmOLD 1628  sbco2 1629  sbcom 1632  sbcom2 1724  sbal1 1737  ax11eq 1754  ax11el 1755  ax11inda 1762  a12lem1 1767  eujustALT 1774  mopick 1833  rgen2aOLD 2161  ralcom2 2244  ralcom2OLD 2245  ceqsalg 2314  reu6 2443  sbcralt 2527  sbcrext 2528  sbcralgf 2529  sbcrexgf 2530  csbie2t 2578  csbnestg 2581  sbcnestg 2583  reldisj 2916  moabex 3513  mosubopt 3551  ssopab2 3573  dfid3 3587  alxfr 3836  dmcosseqOLD 4215  fununi 4481  fv3 4690  cbvfo 4861  fnoprabg 4941  pssnn 5628  kmlem16 5942  axextnd 6095  axrepndlem1 6096  axrepndlem2 6097  axunndlem1 6099  axunnd 6100  axpowndlem1 6101  axpowndlem2 6102  axpowndlem3 6103  axpowndlem4 6104  axregndlem1 6106  axregndlem2 6107  axregnd 6108  axinfndlem1 6109  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  axacnd 6116  suppsr3 6376  bnj9 12372  fundmpss 13836  wfrlem5 13961  nalf 14153  uninqs 14340  ref4w 14370  pospos 14635  cmphmp 14878  qusp 14908  bwt2 14960  imonclem 15162  pm10.55 16316  2albi 16330  pm11.57 16346  ax4567to6 16362  ax10ext 16364  ax10-16 16365  pm14.122b 16387  pm14.123b 16390  eupickbi 16400  cla4gft 16406  dropab1 16424  dropab2 16425

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

Copyright terms: Public domain