Theorem ibi 176

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  ibir  177  pm5.21nii  716  elab3gf  2976  elpwi  3698  elsni  3727  elpr2  3731  elpri  3732  eltpi  3756  snssi  3859  prssi  3873  eloni  4520  limuni2  4542  elxpi  4790  releldmb  5019  relelrnb  5020  elrnmpt2d  5037  elrelimasn  5153  funeu  5402  fneu  5487  fvelima  5754  eloprabi  6432  fo2ndf  6463  elmpom  6474  fczsupp0  6499  tfrlem9  6590  ecexr  6812  elqsi  6861  qsel  6886  ecopovsym  6905  ecopovsymg  6908  elpmi  6941  elmapi  6944  pmsspw  6964  brdomi  7033  en1uniel  7091  mapdom1g  7147  dif1en  7183  enomnilem  7479  omnimkv  7497  mkvprop  7499  fodjumkvlemres  7500  enmkvlem  7502  enwomnilem  7510  ltrnqi  7789  peano2nnnn  8221  peano2nn  9319  eliooord  10341  fzrev3i  10506  elfzole1  10574  elfzolt2  10575  bcp1nk  11216  rere  11646  climcl  12067  climcau  12132  fprodcnv  12411  isstruct2im  13414  restsspw  13656  mgmcl  13732  submss  13836  subm0cl  13838  submcl  13839  submmnd  13840  subgsubm  14052  ringidval  14349  opprnzr  14577  opprdomn  14668  zrhval  15036  istopfin  15192  uniopn  15193  iunopn  15194  inopn  15195  eltpsg  15232  basis1  15239  basis2  15240  eltg4i  15247  lmff  15441  psmetf  15517  psmet0  15519  psmettri2  15520  metflem  15541  xmetf  15542  xmeteq0  15551  xmettri2  15553  cncff  15769  cncfi  15770  limcresi  15858  dvcnp2cntop  15891  sinq34lt0t  16024  lgsdir2lem2  16314  2sqlem9  16409  edgval  16467  uhgrfm  16480  ushgrfm  16481  upgrfen  16504  umgrfen  16514  uspgrfen  16566  usgrfen  16567  wlkcprim  16757  trlsv  16791  isclwwlkni  16814  eupthv  16853