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  694  elpr2  3582  eusv2i  4414  ffdm  5339  ov  5937  ovg  5956  nnacl  6424  elpm2r  6608  ltnqpri  7508  ltxrlt  7937  uzaddcl  9491  expcllem  10423  qexpclz  10433  1exp  10441  facnn  10594  fac0  10595  fac1  10596  bcn2  10631  znnen  12110