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  2990  elimhyp  3710  elimhyp2v  3711  elimhyp3v  3712  elimhyp4v  3713  elpwi  3730  elpr2  3752  elpri  3753  elsni  3757  eltpi  3770  snssi  3852  prssi  3863  evennn  4506  oddnn  4507  evennnul  4508  oddnnul  4509  sucevenodd  4510  sucoddeven  4511  eventfin  4517  oddtfin  4518  nnadjoin  4520  nnadjoinpw  4521  elxpi  4800  elfunsi  5831  trd  5921  frd  5922  extd  5923  symd  5924  refd  5927  antid  5929  connexd  5931  elqsi  5978  pmfun  6015  elmapi  6016  cannc  6333  cantc  6336