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  706  elpr2  3655  eusv2i  4503  ffdm  5448  ov  6067  ovg  6087  nnacl  6568  elpm2r  6755  ltnqpri  7709  ltxrlt  8140  uzaddcl  9709  expcllem  10697  qexpclz  10707  1exp  10715  facnn  10874  fac0  10875  fac1  10876  bcn2  10911  hash2en  10990  znnen  12802  zrhval  14412