Theorem ibir 177

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.21nii  716  elpr2  3731  eusv2i  4601  ffdm  5558  ov  6208  ovg  6228  nnacl  6753  elpm2r  6940  ltnqpri  7961  ltxrlt  8391  uzaddcl  9986  fzspl  10476  expcllem  10987  qexpclz  10997  1exp  11005  facnn  11165  fac0  11166  fac1  11167  bcn2  11202  en1hash  11239  hash2en  11295  znnen  13289  zrhval  14952