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-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ibir  176  pm5.21nii  693  elab3gf  2829  elpwi  3514  elsni  3540  elpr2  3544  elpri  3545  eltpi  3565  snssi  3659  prssi  3673  eloni  4292  limuni2  4314  elxpi  4550  releldmb  4771  relelrnb  4772  elrnmpt2d  4789  funeu  5143  fneu  5222  fvelima  5466  eloprabi  6087  fo2ndf  6117  tfrlem9  6209  ecexr  6427  elqsi  6474  qsel  6499  ecopovsym  6518  ecopovsymg  6521  elpmi  6554  elmapi  6557  pmsspw  6570  brdomi  6636  en1uniel  6691  mapdom1g  6734  dif1en  6766  enomnilem  7003  omnimkv  7023  mkvprop  7025  fodjumkvlemres  7026  ltrnqi  7222  peano2nnnn  7654  peano2nn  8725  eliooord  9704  fzrev3i  9861  elfzole1  9925  elfzolt2  9926  bcp1nk  10501  rere  10630  climcl  11044  climcau  11109  isstruct2im  11958  restsspw  12119  istopfin  12156  uniopn  12157  iunopn  12158  inopn  12159  eltpsg  12196  basis1  12203  basis2  12204  eltg4i  12213  lmff  12407  psmetf  12483  psmet0  12485  psmettri2  12486  metflem  12507  xmetf  12508  xmeteq0  12517  xmettri2  12519  cncff  12722  cncfi  12723  limcresi  12793  dvcnp2cntop  12821  sinq34lt0t  12901