Theorem mpg 986

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

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  mpgbi 987  mpgbir 988  a5i 989  albii 999  hbn 1004  19.9 1036  19.22i 1040  exbii 1051  ax9 1124  cbv3 1164  cbval 1165  chvar 1167  sbt 1192  equsb1 1193  equsb2 1194  chvarv 1327  immoi 1418  2eumo 1442  vtoclf 1841  vtocl2 1843  vtocl3 1844  euxfr2 1926  axsep 2702  axnul2 2708  dtrucor 2773  tz9.13 4663  ac7 4748  axpowndlem3 4951  infxpidmlem9 7560

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

Copyright terms: Public domain