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  699  elpr2  3605  eusv2i  4440  ffdm  5368  ov  5972  ovg  5991  nnacl  6459  elpm2r  6644  ltnqpri  7556  ltxrlt  7985  uzaddcl  9545  expcllem  10487  qexpclz  10497  1exp  10505  facnn  10661  fac0  10662  fac1  10663  bcn2  10698  znnen  12353