Theorem ibir 175

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

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.21nii  653  elpr2  3439  eusv2i  4234  ffdm  5113  ov  5672  ovg  5691  nnacl  6145  ltnqpri  6882  ltxrlt  7281  uzaddcl  8791  expcllem  9620  qexpclz  9630  1exp  9638  facnn  9787  fac0  9788  fac1  9789  bcn2  9824  znnen  10802