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  694  elab3gf  2876  elpwi  3568  elsni  3594  elpr2  3598  elpri  3599  eltpi  3623  snssi  3717  prssi  3731  eloni  4353  limuni2  4375  elxpi  4620  releldmb  4841  relelrnb  4842  elrnmpt2d  4859  funeu  5213  fneu  5292  fvelima  5538  eloprabi  6164  fo2ndf  6195  tfrlem9  6287  ecexr  6506  elqsi  6553  qsel  6578  ecopovsym  6597  ecopovsymg  6600  elpmi  6633  elmapi  6636  pmsspw  6649  brdomi  6715  en1uniel  6770  mapdom1g  6813  dif1en  6845  enomnilem  7102  omnimkv  7120  mkvprop  7122  fodjumkvlemres  7123  enmkvlem  7125  enwomnilem  7133  ltrnqi  7362  peano2nnnn  7794  peano2nn  8869  eliooord  9864  fzrev3i  10023  elfzole1  10090  elfzolt2  10091  bcp1nk  10675  rere  10807  climcl  11223  climcau  11288  fprodcnv  11566  isstruct2im  12404  restsspw  12566  mgmcl  12590  istopfin  12638  uniopn  12639  iunopn  12640  inopn  12641  eltpsg  12678  basis1  12685  basis2  12686  eltg4i  12695  lmff  12889  psmetf  12965  psmet0  12967  psmettri2  12968  metflem  12989  xmetf  12990  xmeteq0  12999  xmettri2  13001  cncff  13204  cncfi  13205  limcresi  13275  dvcnp2cntop  13303  sinq34lt0t  13392  lgsdir2lem2  13570  2sqlem9  13600