Theorem mpg 962

Description: Modus ponens combined with generalization.

Hypotheses

Ref	Expression
mpg.1	|- (A.xph -> ps)
mpg.2	|- ph

Assertion

Ref	Expression
mpg	|- ps

Proof of Theorem mpg

Step	Hyp	Ref	Expression
1		mpg.2	. . 3 |- ph
2	1	ax-gen 955	. 2 |- A.xph
3		mpg.1	. 2 |- (A.xph -> ps)
4	2, 3	ax-mp 7	1 |- ps

Syntax hints:   -> wi 3  A.wal 950

This theorem is referenced by:  mpgbi 963  mpgbir 964  a5i 965  albii 975  hbn 980  19.9 1012  19.22i 1016  exbii 1027  ax9a 1111  cbv3 1147  cbval 1148  chvar 1150  sbt 1175  equsb1 1176  equsb2 1177  chvarv 1309  immoi 1395  2eumo 1419  vtoclf 1816  vtocl2 1818  vtocl3 1819  euxfr2 1897  axsep 2670  axnul2 2676  dtrucor 2741  tz9.13 4587  ac7 4672  axpowndlem3 4874  infxpidmlem9 7454

This theorem was proved from axioms:  ax-mp 7  ax-gen 955

Copyright terms: Public domain