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  9995  fzspl  10486  expcllem  11000  qexpclz  11010  1exp  11018  facnn  11179  fac0  11180  fac1  11181  bcn2  11216  en1hash  11253  hash2en  11309  znnen  13338  zrhval  15001