Theorem mpg 1170

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

Syntax hints:   -> wi 3  A.wal 1134

This theorem is referenced by:  a5i 1173  albii 1184  hbn 1189  19.9 1221  eximi 1225  exbii 1236  ax9 1320  cbv3 1363  cbv3ALT 1364  cbvalOLD 1366  chvar 1368  sbtOLD 1398  equsb1 1399  equsb2 1400  chvarv 1550  immoi 1651  2eumo 1683  r19.21v 2012  vtoclf 2171  vtocl2 2173  vtocl2OLD 2174  vtocl3 2175  vtocl3OLD 2176  euxfr2 2270  csbex 2382  axsep 3252  axnulALT 3258  dtrucor 3333  eufnfv 4582  reiota4 4918  ac6sfilem1 5317  riotav 5376  riotabiia 5386  ordtypelem6 5499  tz9.13 5583  ac7 5706  axpowndlem3 5899  infxpidmlem9 8624  bnj159 12276  bnj165 12285  bnj166 12286  bnj586 12344  bnj98 13013  setinds 13635  hbng 13666  ordtypelem6OLD 15062  pm11.11 16005  sbeqal1i 16038  ax4567to6 16044  ax4567to7 16045  iota2 16075  stbbi 16485

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

Copyright terms: Public domain