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 )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21nii  709  elpr2  3688  eusv2i  4546  ffdm  5494  ov  6124  ovg  6144  nnacl  6626  elpm2r  6813  ltnqpri  7781  ltxrlt  8212  uzaddcl  9781  expcllem  10772  qexpclz  10782  1exp  10790  facnn  10949  fac0  10950  fac1  10951  bcn2  10986  hash2en  11065  znnen  12969  zrhval  14581