Theorem ibi 232

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.)

Hypothesis

Ref	Expression
ibi.1	|- (ph -> (ph <-> ps))

Assertion

Ref	Expression
ibi	|- (ph -> ps)

Proof of Theorem ibi

Step	Hyp	Ref	Expression
1		ibi.1	. . 3 |- (ph -> (ph <-> ps))
2	1	biimpd 198	. 2 |- (ph -> (ph -> ps))
3	2	pm2.43i 43	1 |- (ph -> ps)

Syntax hints:   -> wi 4   <-> wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  ibir  233  elimh  922  elab3gf  2991  elimhyp  3711  elimhyp2v  3712  elimhyp3v  3713  elimhyp4v  3714  elpwi  3731  elpr2  3753  elpri  3754  elsni  3758  eltpi  3771  snssi  3853  prssi  3864  evennn  4507  oddnn  4508  evennnul  4509  oddnnul  4510  sucevenodd  4511  sucoddeven  4512  eventfin  4518  oddtfin  4519  nnadjoin  4521  nnadjoinpw  4522  elxpi  4801  elfunsi  5832  trd  5922  frd  5923  extd  5924  symd  5925  refd  5928  antid  5930  connexd  5932  elqsi  5979  pmfun  6016  elmapi  6017  cannc  6334  cantc  6337