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  652  elpr2  3420  eusv2i  4205  ffdm  5081  ov  5640  ovg  5659  nnacl  6082  ltnqpri  6784  ltxrlt  7178  uzaddcl  8674  expcllem  9487  qexpclz  9497  1exp  9505  facnn  9654  fac0  9655  fac1  9656  bcn2  9691