Theorem mpg 1022

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

Syntax hints:   -> wi 3  A.wal 990

This theorem is referenced by:  a5i 1025  albii 1035  hbn 1040  19.9 1072  19.22i 1076  exbii 1087  ax9 1160  cbv3 1201  cbval 1202  chvar 1204  sbt 1229  equsb1 1230  equsb2 1231  chvarv 1365  immoi 1457  2eumo 1482  vtoclf 1887  vtocl2 1889  vtocl3 1890  euxfr2 1972  axsep 2776  axnul2 2782  dtrucor 2849  ac6sfilem1 4588  tz9.13 4809  ac7 4894  axpowndlem3 5105  infxpidmlem9 7772  ordtypelem6 11432

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

Copyright terms: Public domain