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  709  elab3gf  2954  elpwi  3659  elsni  3685  elpr2  3689  elpri  3690  eltpi  3714  snssi  3815  prssi  3829  eloni  4470  limuni2  4492  elxpi  4739  releldmb  4967  relelrnb  4968  elrnmpt2d  4985  elrelimasn  5100  funeu  5349  fneu  5433  fvelima  5693  eloprabi  6356  fo2ndf  6387  elmpom  6398  tfrlem9  6480  ecexr  6702  elqsi  6751  qsel  6776  ecopovsym  6795  ecopovsymg  6798  elpmi  6831  elmapi  6834  pmsspw  6847  brdomi  6915  en1uniel  6973  mapdom1g  7028  dif1en  7061  enomnilem  7328  omnimkv  7346  mkvprop  7348  fodjumkvlemres  7349  enmkvlem  7351  enwomnilem  7359  ltrnqi  7631  peano2nnnn  8063  peano2nn  9145  eliooord  10153  fzrev3i  10313  elfzole1  10381  elfzolt2  10382  bcp1nk  11014  rere  11416  climcl  11833  climcau  11898  fprodcnv  12176  isstruct2im  13082  restsspw  13322  mgmcl  13432  submss  13549  subm0cl  13551  submcl  13552  submmnd  13553  subgsubm  13773  opprnzr  14190  opprdomn  14279  zrhval  14621  istopfin  14714  uniopn  14715  iunopn  14716  inopn  14717  eltpsg  14754  basis1  14761  basis2  14762  eltg4i  14769  lmff  14963  psmetf  15039  psmet0  15041  psmettri2  15042  metflem  15063  xmetf  15064  xmeteq0  15073  xmettri2  15075  cncff  15291  cncfi  15292  limcresi  15380  dvcnp2cntop  15413  sinq34lt0t  15545  lgsdir2lem2  15748  2sqlem9  15843  edgval  15901  uhgrfm  15914  ushgrfm  15915  upgrfen  15938  umgrfen  15948  uspgrfen  15998  usgrfen  15999  wlkcprim  16147  trlsv  16179  isclwwlkni  16202  eupthv  16241