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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  ibir  177  pm5.21nii  716  elab3gf  2976  elpwi  3698  elsni  3727  elpr2  3731  elpri  3732  eltpi  3756  snssi  3859  prssi  3873  eloni  4520  limuni2  4542  elxpi  4790  releldmb  5019  relelrnb  5020  elrnmpt2d  5037  elrelimasn  5153  funeu  5402  fneu  5487  fvelima  5754  eloprabi  6432  fo2ndf  6463  elmpom  6474  fczsupp0  6499  tfrlem9  6590  ecexr  6812  elqsi  6861  qsel  6886  ecopovsym  6905  ecopovsymg  6908  elpmi  6941  elmapi  6944  pmsspw  6964  brdomi  7033  en1uniel  7091  mapdom1g  7147  dif1en  7183  enomnilem  7478  omnimkv  7496  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  enwomnilem  7509  ltrnqi  7788  peano2nnnn  8220  peano2nn  9318  eliooord  10340  fzrev3i  10505  elfzole1  10573  elfzolt2  10574  bcp1nk  11214  rere  11644  climcl  12064  climcau  12129  fprodcnv  12408  isstruct2im  13411  restsspw  13652  mgmcl  13728  submss  13832  subm0cl  13834  submcl  13835  submmnd  13836  subgsubm  14048  ringidval  14314  opprnzr  14542  opprdomn  14633  zrhval  15001  istopfin  15150  uniopn  15151  iunopn  15152  inopn  15153  eltpsg  15190  basis1  15197  basis2  15198  eltg4i  15205  lmff  15399  psmetf  15475  psmet0  15477  psmettri2  15478  metflem  15499  xmetf  15500  xmeteq0  15509  xmettri2  15511  cncff  15727  cncfi  15728  limcresi  15816  dvcnp2cntop  15849  sinq34lt0t  15982  lgsdir2lem2  16246  2sqlem9  16341  edgval  16399  uhgrfm  16412  ushgrfm  16413  upgrfen  16436  umgrfen  16446  uspgrfen  16498  usgrfen  16499  wlkcprim  16689  trlsv  16723  isclwwlkni  16746  eupthv  16785