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  2465  nfci  2480  abid2f  2515  rgen  2680  ssriv  3278  ss2abi  3339  ssmin  3946  intab  3957  iunab  4013  iinab  4028  nincompl  4073  peano1  4403  addcnul1  4453  ncvspfin  4539  xpvv  4844  relssi  4849  eqrelriv  4851  eqoprriv  4854  dm0  4919  dmi  4920  co01  5094  ssdmrn  5100  funopabeq  5141  funsn  5148  fvopab3ig  5388  1stfo  5506  2ndfo  5507  swapf1o  5512  dmep  5525  caovmo  5646  fnfullfunlem2  5858  fvfullfunlem3  5864  clos1is  5882