Theorem mpgbi 1333

Description: Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)

Hypotheses

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

Assertion

Ref	Expression
mpgbi	|- ps

Proof of Theorem mpgbi

Step	Hyp	Ref	Expression
1		mpgbi.2	. . 3 |- ph
2	1	ax-gen 1305	. 2 |- A.xph
3		mpgbi.1	. 2 |- (A.xph <-> ps)
4	2, 3	mpbi 206	1 |- ps

Syntax hints:   <-> wb 163  A.wal 1296

This theorem is referenced by:  19.23ai 1412  nex 1456  exan 1463  exanOLD 1464  csbief 2576  nalset 3448  ordtypelem7 5690  ac4 5912  ac8 5925  ackm 5944  bnj23 12397  bnj872 12800  bnj1036 12886  bnj1221 12996  bnj1031 13383  ordtypelem7OLD 15381  neibastop2 15523  neibastop3 15524  ist1-3 15543

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain