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  699  elab3gf  2880  elpwi  3575  elsni  3601  elpr2  3605  elpri  3606  eltpi  3630  snssi  3724  prssi  3738  eloni  4360  limuni2  4382  elxpi  4627  releldmb  4848  relelrnb  4849  elrnmpt2d  4866  funeu  5223  fneu  5302  fvelima  5548  eloprabi  6175  fo2ndf  6206  tfrlem9  6298  ecexr  6518  elqsi  6565  qsel  6590  ecopovsym  6609  ecopovsymg  6612  elpmi  6645  elmapi  6648  pmsspw  6661  brdomi  6727  en1uniel  6782  mapdom1g  6825  dif1en  6857  enomnilem  7114  omnimkv  7132  mkvprop  7134  fodjumkvlemres  7135  enmkvlem  7137  enwomnilem  7145  ltrnqi  7383  peano2nnnn  7815  peano2nn  8890  eliooord  9885  fzrev3i  10044  elfzole1  10111  elfzolt2  10112  bcp1nk  10696  rere  10829  climcl  11245  climcau  11310  fprodcnv  11588  isstruct2im  12426  restsspw  12589  mgmcl  12613  submss  12698  subm0cl  12700  submcl  12701  istopfin  12792  uniopn  12793  iunopn  12794  inopn  12795  eltpsg  12832  basis1  12839  basis2  12840  eltg4i  12849  lmff  13043  psmetf  13119  psmet0  13121  psmettri2  13122  metflem  13143  xmetf  13144  xmeteq0  13153  xmettri2  13155  cncff  13358  cncfi  13359  limcresi  13429  dvcnp2cntop  13457  sinq34lt0t  13546  lgsdir2lem2  13724  2sqlem9  13754