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  2914  elpwi  3615  elsni  3641  elpr2  3645  elpri  3646  eltpi  3670  snssi  3767  prssi  3781  eloni  4411  limuni2  4433  elxpi  4680  releldmb  4904  relelrnb  4905  elrnmpt2d  4922  elrelimasn  5036  funeu  5284  fneu  5365  fvelima  5615  eloprabi  6263  fo2ndf  6294  tfrlem9  6386  ecexr  6606  elqsi  6655  qsel  6680  ecopovsym  6699  ecopovsymg  6702  elpmi  6735  elmapi  6738  pmsspw  6751  brdomi  6817  en1uniel  6872  mapdom1g  6917  dif1en  6949  enomnilem  7213  omnimkv  7231  mkvprop  7233  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  ltrnqi  7507  peano2nnnn  7939  peano2nn  9021  eliooord  10022  fzrev3i  10182  elfzole1  10250  elfzolt2  10251  bcp1nk  10873  rere  11049  climcl  11466  climcau  11531  fprodcnv  11809  isstruct2im  12715  restsspw  12953  mgmcl  13063  submss  13180  subm0cl  13182  submcl  13183  submmnd  13184  subgsubm  13404  opprnzr  13820  opprdomn  13909  zrhval  14251  istopfin  14344  uniopn  14345  iunopn  14346  inopn  14347  eltpsg  14384  basis1  14391  basis2  14392  eltg4i  14399  lmff  14593  psmetf  14669  psmet0  14671  psmettri2  14672  metflem  14693  xmetf  14694  xmeteq0  14703  xmettri2  14705  cncff  14921  cncfi  14922  limcresi  15010  dvcnp2cntop  15043  sinq34lt0t  15175  lgsdir2lem2  15378  2sqlem9  15473