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  705  elab3gf  2902  elpwi  3599  elsni  3625  elpr2  3629  elpri  3630  eltpi  3654  snssi  3751  prssi  3765  eloni  4393  limuni2  4415  elxpi  4660  releldmb  4882  relelrnb  4883  elrnmpt2d  4900  elrelimasn  5012  funeu  5260  fneu  5339  fvelima  5588  eloprabi  6221  fo2ndf  6252  tfrlem9  6344  ecexr  6564  elqsi  6613  qsel  6638  ecopovsym  6657  ecopovsymg  6660  elpmi  6693  elmapi  6696  pmsspw  6709  brdomi  6775  en1uniel  6830  mapdom1g  6875  dif1en  6907  enomnilem  7166  omnimkv  7184  mkvprop  7186  fodjumkvlemres  7187  enmkvlem  7189  enwomnilem  7197  ltrnqi  7450  peano2nnnn  7882  peano2nn  8961  eliooord  9958  fzrev3i  10118  elfzole1  10185  elfzolt2  10186  bcp1nk  10774  rere  10906  climcl  11322  climcau  11387  fprodcnv  11665  isstruct2im  12522  restsspw  12754  mgmcl  12835  submss  12928  subm0cl  12930  submcl  12931  submmnd  12932  subgsubm  13135  istopfin  13960  uniopn  13961  iunopn  13962  inopn  13963  eltpsg  14000  basis1  14007  basis2  14008  eltg4i  14015  lmff  14209  psmetf  14285  psmet0  14287  psmettri2  14288  metflem  14309  xmetf  14310  xmeteq0  14319  xmettri2  14321  cncff  14524  cncfi  14525  limcresi  14595  dvcnp2cntop  14623  sinq34lt0t  14712  lgsdir2lem2  14891  2sqlem9  14932