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  705  elab3gf  2899  elpwi  3596  elsni  3622  elpr2  3626  elpri  3627  eltpi  3651  snssi  3748  prssi  3762  eloni  4387  limuni2  4409  elxpi  4654  releldmb  4876  relelrnb  4877  elrnmpt2d  4894  elrelimasn  5006  funeu  5253  fneu  5332  fvelima  5580  eloprabi  6210  fo2ndf  6241  tfrlem9  6333  ecexr  6553  elqsi  6600  qsel  6625  ecopovsym  6644  ecopovsymg  6647  elpmi  6680  elmapi  6683  pmsspw  6696  brdomi  6762  en1uniel  6817  mapdom1g  6860  dif1en  6892  enomnilem  7149  omnimkv  7167  mkvprop  7169  fodjumkvlemres  7170  enmkvlem  7172  enwomnilem  7180  ltrnqi  7433  peano2nnnn  7865  peano2nn  8944  eliooord  9941  fzrev3i  10101  elfzole1  10168  elfzolt2  10169  bcp1nk  10755  rere  10887  climcl  11303  climcau  11368  fprodcnv  11646  isstruct2im  12485  restsspw  12715  mgmcl  12796  submss  12888  subm0cl  12890  submcl  12891  subgsubm  13087  istopfin  13771  uniopn  13772  iunopn  13773  inopn  13774  eltpsg  13811  basis1  13818  basis2  13819  eltg4i  13826  lmff  14020  psmetf  14096  psmet0  14098  psmettri2  14099  metflem  14120  xmetf  14121  xmeteq0  14130  xmettri2  14132  cncff  14335  cncfi  14336  limcresi  14406  dvcnp2cntop  14434  sinq34lt0t  14523  lgsdir2lem2  14701  2sqlem9  14742