Theorem mpg 983

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 960	. 2 |- A.xph
3		mpg.1	. 2 |- (A.xph -> ps)
4	2, 3	ax-mp 7	1 |- ps

Syntax hints:   -> wi 3  A.wal 951

This theorem is referenced by:  mpgbi 984  mpgbir 985  a5i 986  albii 996  hbn 1001  19.9 1032  19.22i 1036  exbii 1047  ax9 1120  cbv3 1160  cbval 1161  chvar 1163  sbt 1188  equsb1 1189  equsb2 1190  chvarv 1322  immoi 1411  2eumo 1435  vtoclf 1832  vtocl2 1834  vtocl3 1835  euxfr2 1916  axsep 2692  axnul2 2698  dtrucor 2763  tz9.13 4635  ac7 4720  axpowndlem3 4923  infxpidmlem9 7503

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

Copyright terms: Public domain