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  6757  elpm2r  6944  ltnqpri  7967  ltxrlt  8397  uzaddcl  10002  fzspl  10493  expcllem  11008  qexpclz  11018  1exp  11026  facnn  11187  fac0  11188  fac1  11189  bcn2  11224  en1hash  11261  hash2en  11317  znnen  13347  zrhval  15061