Theorem ibir 257

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)

Hypothesis

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

Assertion

Ref	Expression
ibir	|- ( ph -> ps )

Proof of Theorem ibir

Step	Hyp	Ref	Expression
1		ibir.1	. . 3 |- ( ph -> ( ps <-> ph ) )
2	1	bicomd 213	. 2 |- ( ph -> ( ph <-> ps ) )
3	2	ibi 256	1 |- ( ph -> ps )

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

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 197

This theorem is referenced by:  elpr2OLD  4200  eusv2i  4863  ffdm  6062  ov  6780  ovg  6799  oacl  7615  nnacl  7691  elpm2r  7875  cdaxpdom  9011  cdafi  9012  cfcof  9096  hargch  9495  uzaddcl  11744  expcllem  12871  lcmfval  15334  lcmf0val  15335  mreunirn  16261  filunirn  21686  ustelimasn  22026  metustfbas  22362  usgreqdrusgr  26464  pjini  28558  fzspl  29550  f1ocnt  29559  xrge0tsmsbi  29786  bnj983  31021  poimirlem16  33425  poimirlem19  33428  poimirlem25  33434  ac6s6  33980  fouriersw  40448  etransclem25  40476  bits0oALTV  41592  uzlidlring  41929  linccl  42203