Theorem ibir 176

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 140	. 2 |- ( ph -> ( ph <-> ps ) )
3	2	ibi 175	1 |- ( ph -> ps )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.21nii  694  elpr2  3598  eusv2i  4433  ffdm  5358  ov  5961  ovg  5980  nnacl  6448  elpm2r  6632  ltnqpri  7535  ltxrlt  7964  uzaddcl  9524  expcllem  10466  qexpclz  10476  1exp  10484  facnn  10640  fac0  10641  fac1  10642  bcn2  10677  znnen  12331