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

Assertion

Ref	Expression
ibi	⊢ (𝜑 → 𝜓)

Proof of Theorem ibi

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

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  709  elab3gf  2953  elpwi  3658  elsni  3684  elpr2  3688  elpri  3689  eltpi  3713  snssi  3811  prssi  3825  eloni  4465  limuni2  4487  elxpi  4734  releldmb  4960  relelrnb  4961  elrnmpt2d  4978  elrelimasn  5093  funeu  5342  fneu  5426  fvelima  5684  eloprabi  6340  fo2ndf  6371  tfrlem9  6463  ecexr  6683  elqsi  6732  qsel  6757  ecopovsym  6776  ecopovsymg  6779  elpmi  6812  elmapi  6815  pmsspw  6828  brdomi  6896  en1uniel  6954  mapdom1g  7004  dif1en  7037  enomnilem  7301  omnimkv  7319  mkvprop  7321  fodjumkvlemres  7322  enmkvlem  7324  enwomnilem  7332  ltrnqi  7604  peano2nnnn  8036  peano2nn  9118  eliooord  10120  fzrev3i  10280  elfzole1  10348  elfzolt2  10349  bcp1nk  10979  rere  11371  climcl  11788  climcau  11853  fprodcnv  12131  isstruct2im  13037  restsspw  13277  mgmcl  13387  submss  13504  subm0cl  13506  submcl  13507  submmnd  13508  subgsubm  13728  opprnzr  14144  opprdomn  14233  zrhval  14575  istopfin  14668  uniopn  14669  iunopn  14670  inopn  14671  eltpsg  14708  basis1  14715  basis2  14716  eltg4i  14723  lmff  14917  psmetf  14993  psmet0  14995  psmettri2  14996  metflem  15017  xmetf  15018  xmeteq0  15027  xmettri2  15029  cncff  15245  cncfi  15246  limcresi  15334  dvcnp2cntop  15367  sinq34lt0t  15499  lgsdir2lem2  15702  2sqlem9  15797  uhgrfm  15867  ushgrfm  15868  upgrfen  15891  umgrfen  15901  uspgrfen  15951  usgrfen  15952