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 )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ibir  177  pm5.21nii  706  elab3gf  2923  elpwi  3625  elsni  3651  elpr2  3655  elpri  3656  eltpi  3680  snssi  3777  prssi  3791  eloni  4423  limuni2  4445  elxpi  4692  releldmb  4916  relelrnb  4917  elrnmpt2d  4934  elrelimasn  5049  funeu  5297  fneu  5381  fvelima  5632  eloprabi  6284  fo2ndf  6315  tfrlem9  6407  ecexr  6627  elqsi  6676  qsel  6701  ecopovsym  6720  ecopovsymg  6723  elpmi  6756  elmapi  6759  pmsspw  6772  brdomi  6840  en1uniel  6898  mapdom1g  6946  dif1en  6978  enomnilem  7242  omnimkv  7260  mkvprop  7262  fodjumkvlemres  7263  enmkvlem  7265  enwomnilem  7273  ltrnqi  7536  peano2nnnn  7968  peano2nn  9050  eliooord  10052  fzrev3i  10212  elfzole1  10280  elfzolt2  10281  bcp1nk  10909  rere  11209  climcl  11626  climcau  11691  fprodcnv  11969  isstruct2im  12875  restsspw  13114  mgmcl  13224  submss  13341  subm0cl  13343  submcl  13344  submmnd  13345  subgsubm  13565  opprnzr  13981  opprdomn  14070  zrhval  14412  istopfin  14505  uniopn  14506  iunopn  14507  inopn  14508  eltpsg  14545  basis1  14552  basis2  14553  eltg4i  14560  lmff  14754  psmetf  14830  psmet0  14832  psmettri2  14833  metflem  14854  xmetf  14855  xmeteq0  14864  xmettri2  14866  cncff  15082  cncfi  15083  limcresi  15171  dvcnp2cntop  15204  sinq34lt0t  15336  lgsdir2lem2  15539  2sqlem9  15634