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  693  elpr2  3549  eusv2i  4376  ffdm  5293  ov  5890  ovg  5909  nnacl  6376  elpm2r  6560  ltnqpri  7402  ltxrlt  7830  uzaddcl  9381  expcllem  10304  qexpclz  10314  1exp  10322  facnn  10473  fac0  10474  fac1  10475  bcn2  10510  znnen  11911