Theorem ibi 174

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.)

Hypothesis

Ref	Expression
ibi.1	|- ( ph -> ( ph <-> ps ) )

Assertion

Ref	Expression
ibi	|- ( ph -> ps )

Proof of Theorem ibi

Step	Hyp	Ref	Expression
1		ibi.1	. . 3 |- ( ph -> ( ph <-> ps ) )
2	1	biimpd 142	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 48	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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ibir  175  pm5.21nii  653  elab3gf  2744  elpwi  3393  elsni  3418  elpr2  3422  elpri  3423  eltpi  3441  snssi  3531  prssi  3545  eloni  4132  limuni2  4154  elxpi  4381  releldmb  4593  relelrnb  4594  funeu  4950  fneu  5028  fvelima  5251  eloprabi  5847  fo2ndf  5873  tfrlem9  5962  ecexr  6170  elqsi  6217  qsel  6242  ecopovsym  6261  ecopovsymg  6264  brdomi  6289  en1uniel  6343  dif1en  6404  ltrnqi  6662  peano2nnnn  7072  peano2nn  8107  eliooord  9016  fzrev3i  9170  elfzole1  9230  elfzolt2  9231  bcp1nk  9775  rere  9879  climcl  10248  climcau  10311