Theorem ibi 174

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 142	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 48	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ibir  175  pm5.21nii  652  elab3gf  2743  elpwi  3391  elsni  3416  elpr2  3420  elpri  3421  eltpi  3439  snssi  3529  prssi  3543  eloni  4130  limuni2  4152  elxpi  4379  releldmb  4589  relelrnb  4590  funeu  4946  fneu  5023  fvelima  5246  eloprabi  5842  fo2ndf  5868  tfrlem9  5958  ecexr  6134  elqsi  6181  qsel  6206  ecopovsym  6225  ecopovsymg  6228  brdomi  6253  en1uniel  6307  dif1en  6364  ltrnqi  6611  peano2nnnn  7021  peano2nn  8051  eliooord  8951  fzrev3i  9105  elfzole1  9164  elfzolt2  9165  bcp1nk  9689  rere  9752  climcl  10121  climcau  10184