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  705  elpr2  3640  eusv2i  4486  ffdm  5424  ov  6038  ovg  6057  nnacl  6533  elpm2r  6720  ltnqpri  7654  ltxrlt  8085  uzaddcl  9651  expcllem  10621  qexpclz  10631  1exp  10639  facnn  10798  fac0  10799  fac1  10800  bcn2  10835  znnen  12555  zrhval  14105