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  4422  limuni2  4444  elxpi  4691  releldmb  4915  relelrnb  4916  elrnmpt2d  4933  elrelimasn  5048  funeu  5296  fneu  5380  fvelima  5630  eloprabi  6282  fo2ndf  6313  tfrlem9  6405  ecexr  6625  elqsi  6674  qsel  6699  ecopovsym  6718  ecopovsymg  6721  elpmi  6754  elmapi  6757  pmsspw  6770  brdomi  6838  en1uniel  6896  mapdom1g  6944  dif1en  6976  enomnilem  7240  omnimkv  7258  mkvprop  7260  fodjumkvlemres  7261  enmkvlem  7263  enwomnilem  7271  ltrnqi  7534  peano2nnnn  7966  peano2nn  9048  eliooord  10050  fzrev3i  10210  elfzole1  10278  elfzolt2  10279  bcp1nk  10907  rere  11176  climcl  11593  climcau  11658  fprodcnv  11936  isstruct2im  12842  restsspw  13081  mgmcl  13191  submss  13308  subm0cl  13310  submcl  13311  submmnd  13312  subgsubm  13532  opprnzr  13948  opprdomn  14037  zrhval  14379  istopfin  14472  uniopn  14473  iunopn  14474  inopn  14475  eltpsg  14512  basis1  14519  basis2  14520  eltg4i  14527  lmff  14721  psmetf  14797  psmet0  14799  psmettri2  14800  metflem  14821  xmetf  14822  xmeteq0  14831  xmettri2  14833  cncff  15049  cncfi  15050  limcresi  15138  dvcnp2cntop  15171  sinq34lt0t  15303  lgsdir2lem2  15506  2sqlem9  15601