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  712  elab3gf  2957  elpwi  3665  elsni  3691  elpr2  3695  elpri  3696  eltpi  3720  snssi  3822  prssi  3836  eloni  4478  limuni2  4500  elxpi  4747  releldmb  4975  relelrnb  4976  elrnmpt2d  4993  elrelimasn  5109  funeu  5358  fneu  5443  fvelima  5706  eloprabi  6370  fo2ndf  6401  elmpom  6412  fczsupp0  6437  tfrlem9  6528  ecexr  6750  elqsi  6799  qsel  6824  ecopovsym  6843  ecopovsymg  6846  elpmi  6879  elmapi  6882  pmsspw  6895  brdomi  6963  en1uniel  7021  mapdom1g  7076  dif1en  7111  enomnilem  7380  omnimkv  7398  mkvprop  7400  fodjumkvlemres  7401  enmkvlem  7403  enwomnilem  7411  ltrnqi  7684  peano2nnnn  8116  peano2nn  9197  eliooord  10207  fzrev3i  10368  elfzole1  10436  elfzolt2  10437  bcp1nk  11070  rere  11488  climcl  11905  climcau  11970  fprodcnv  12249  isstruct2im  13155  restsspw  13395  mgmcl  13505  submss  13622  subm0cl  13624  submcl  13625  submmnd  13626  subgsubm  13846  opprnzr  14264  opprdomn  14354  zrhval  14696  istopfin  14794  uniopn  14795  iunopn  14796  inopn  14797  eltpsg  14834  basis1  14841  basis2  14842  eltg4i  14849  lmff  15043  psmetf  15119  psmet0  15121  psmettri2  15122  metflem  15143  xmetf  15144  xmeteq0  15153  xmettri2  15155  cncff  15371  cncfi  15372  limcresi  15460  dvcnp2cntop  15493  sinq34lt0t  15625  lgsdir2lem2  15831  2sqlem9  15926  edgval  15984  uhgrfm  15997  ushgrfm  15998  upgrfen  16021  umgrfen  16031  uspgrfen  16083  usgrfen  16084  wlkcprim  16274  trlsv  16308  isclwwlkni  16331  eupthv  16370