Theorem ibi 175

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ibir  176  pm5.21nii  656  elab3gf  2766  elpwi  3442  elsni  3468  elpr2  3472  elpri  3473  eltpi  3493  snssi  3587  prssi  3601  eloni  4211  limuni2  4233  elxpi  4468  releldmb  4685  relelrnb  4686  funeu  5053  fneu  5131  fvelima  5369  eloprabi  5980  fo2ndf  6006  tfrlem9  6098  ecexr  6311  elqsi  6358  qsel  6383  ecopovsym  6402  ecopovsymg  6405  elpmi  6438  elmapi  6441  pmsspw  6454  brdomi  6520  en1uniel  6575  mapdom1g  6617  dif1en  6649  enomnilem  6855  ltrnqi  7041  peano2nnnn  7451  peano2nn  8495  eliooord  9407  fzrev3i  9563  elfzole1  9627  elfzolt2  9628  bcp1nk  10231  rere  10360  climcl  10731  climcau  10797  isstruct2im  11565  restsspw  11723  istopfin  11760  uniopn  11761  iunopn  11762  inopn  11763  eltpsg  11799  basis1  11806  basis2  11807  eltg4i  11816  cncff  11906  cncfi  11907