Theorem mpgbir 1550

Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)

Hypotheses

Ref	Expression
mpgbir.1	|- (ph <-> A.xps)
mpgbir.2	|- ps

Assertion

Ref	Expression
mpgbir	|- ph

Proof of Theorem mpgbir

Step	Hyp	Ref	Expression
1		mpgbir.2	. . 3 |- ps
2	1	ax-gen 1546	. 2 |- A.xps
3		mpgbir.1	. 2 |- (ph <-> A.xps)
4	2, 3	mpbir 200	1 |- ph

Syntax hints:   <-> wb 176  A.wal 1540

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  nfi  1551  cvjust  2348  eqriv  2350  abbi2i  2464  nfci  2479  abid2f  2514  rgen  2679  ssriv  3277  ss2abi  3338  ssmin  3945  intab  3956  iunab  4012  iinab  4027  nincompl  4072  peano1  4402  addcnul1  4452  ncvspfin  4538  xpvv  4843  relssi  4848  eqrelriv  4850  eqoprriv  4853  dm0  4918  dmi  4919  co01  5093  ssdmrn  5099  funopabeq  5140  funsn  5147  fvopab3ig  5387  1stfo  5505  2ndfo  5506  swapf1o  5511  dmep  5524  caovmo  5645  fnfullfunlem2  5857  fvfullfunlem3  5863  clos1is  5881