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	⊢ (𝜑 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ibi	⊢ (𝜑 → 𝜓)

Proof of Theorem ibi

Step	Hyp	Ref	Expression
1		ibi.1	. . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
2	1	biimpd 143	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 49	1 ⊢ (𝜑 → 𝜓)

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  2862  elpwi  3552  elsni  3578  elpr2  3582  elpri  3583  eltpi  3607  snssi  3701  prssi  3715  eloni  4336  limuni2  4358  elxpi  4603  releldmb  4824  relelrnb  4825  elrnmpt2d  4842  funeu  5196  fneu  5275  fvelima  5521  eloprabi  6145  fo2ndf  6175  tfrlem9  6267  ecexr  6486  elqsi  6533  qsel  6558  ecopovsym  6577  ecopovsymg  6580  elpmi  6613  elmapi  6616  pmsspw  6629  brdomi  6695  en1uniel  6750  mapdom1g  6793  dif1en  6825  enomnilem  7082  omnimkv  7100  mkvprop  7102  fodjumkvlemres  7103  enmkvlem  7105  enwomnilem  7113  ltrnqi  7342  peano2nnnn  7774  peano2nn  8846  eliooord  9833  fzrev3i  9991  elfzole1  10058  elfzolt2  10059  bcp1nk  10640  rere  10769  climcl  11183  climcau  11248  fprodcnv  11526  isstruct2im  12242  restsspw  12403  istopfin  12440  uniopn  12441  iunopn  12442  inopn  12443  eltpsg  12480  basis1  12487  basis2  12488  eltg4i  12497  lmff  12691  psmetf  12767  psmet0  12769  psmettri2  12770  metflem  12791  xmetf  12792  xmeteq0  12801  xmettri2  12803  cncff  13006  cncfi  13007  limcresi  13077  dvcnp2cntop  13105  sinq34lt0t  13194