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  4603  ffdm  5561  ov  6211  ovg  6231  nnacl  6758  elpm2r  6945  ltnqpri  7967  ltxrlt  8397  uzaddcl  10001  fzspl  10492  expcllem  11007  qexpclz  11017  1exp  11025  facnn  11186  fac0  11187  fac1  11188  bcn2  11223  en1hash  11260  hash2en  11316  znnen  13346  zrhval  15060