Theorem ibi 165

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 132	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 43	1 |- ( ph -> ps )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ibir  166  pm5.21nii  620  elab3gf  2692  elpwi  3368  elsni  3393  elpr2  3397  elpri  3398  eltpi  3417  snssi  3508  prssi  3522  eloni  4112  limuni2  4134  elxpi  4361  releldmb  4571  relelrnb  4572  funeu  4926  fneu  5003  fvelima  5225  eloprabi  5822  fo2ndf  5848  tfrlem9  5935  ecexr  6111  elqsi  6158  qsel  6183  ecopovsym  6202  ecopovsymg  6205  brdomi  6230  en1uniel  6284  dif1en  6337  ltrnqi  6519  peano2nnnn  6929  peano2nn  7926  eliooord  8797  fzrev3i  8950  elfzole1  9011  elfzolt2  9012  rere  9465  climcl  9803  climcau  9866