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-1 5  ax-2 6  ax-mp 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  676  elpr2  3513  eusv2i  4334  ffdm  5249  ov  5842  ovg  5861  nnacl  6328  elpm2r  6512  ltnqpri  7344  ltxrlt  7748  uzaddcl  9277  expcllem  10191  qexpclz  10201  1exp  10209  facnn  10360  fac0  10361  fac1  10362  bcn2  10397  znnen  11750