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  655  elab3gf  2765  elpwi  3438  elsni  3464  elpr2  3468  elpri  3469  eltpi  3489  snssi  3581  prssi  3595  eloni  4202  limuni2  4224  elxpi  4454  releldmb  4672  relelrnb  4673  funeu  5040  fneu  5118  fvelima  5356  eloprabi  5966  fo2ndf  5992  tfrlem9  6084  ecexr  6295  elqsi  6342  qsel  6367  ecopovsym  6386  ecopovsymg  6389  elpmi  6422  elmapi  6425  pmsspw  6438  brdomi  6464  en1uniel  6519  mapdom1g  6561  dif1en  6593  enomnilem  6792  ltrnqi  6978  peano2nnnn  7388  peano2nn  8432  eliooord  9344  fzrev3i  9498  elfzole1  9562  elfzolt2  9563  bcp1nk  10166  rere  10295  climcl  10666  climcau  10732  isstruct2im  11500  istopfin  11552  uniopn  11553  iunopn  11554  inopn  11555  cncff  11588  cncfi  11589