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  2838  elpwi  3524  elsni  3550  elpr2  3554  elpri  3555  eltpi  3578  snssi  3672  prssi  3686  eloni  4305  limuni2  4327  elxpi  4563  releldmb  4784  relelrnb  4785  elrnmpt2d  4802  funeu  5156  fneu  5235  fvelima  5481  eloprabi  6102  fo2ndf  6132  tfrlem9  6224  ecexr  6442  elqsi  6489  qsel  6514  ecopovsym  6533  ecopovsymg  6536  elpmi  6569  elmapi  6572  pmsspw  6585  brdomi  6651  en1uniel  6706  mapdom1g  6749  dif1en  6781  enomnilem  7018  omnimkv  7038  mkvprop  7040  fodjumkvlemres  7041  enmkvlem  7043  enwomnilem  7050  ltrnqi  7253  peano2nnnn  7685  peano2nn  8756  eliooord  9741  fzrev3i  9899  elfzole1  9963  elfzolt2  9964  bcp1nk  10540  rere  10669  climcl  11083  climcau  11148  isstruct2im  12008  restsspw  12169  istopfin  12206  uniopn  12207  iunopn  12208  inopn  12209  eltpsg  12246  basis1  12253  basis2  12254  eltg4i  12263  lmff  12457  psmetf  12533  psmet0  12535  psmettri2  12536  metflem  12557  xmetf  12558  xmeteq0  12567  xmettri2  12569  cncff  12772  cncfi  12773  limcresi  12843  dvcnp2cntop  12871  sinq34lt0t  12960