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  4522  limuni2  4544  elxpi  4792  releldmb  5021  relelrnb  5022  elrnmpt2d  5039  elrelimasn  5156  funeu  5405  fneu  5490  fvelima  5757  eloprabi  6436  fo2ndf  6467  elmpom  6478  fczsupp0  6503  tfrlem9  6595  ecexr  6817  elqsi  6866  qsel  6891  ecopovsym  6910  ecopovsymg  6913  elpmi  6946  elmapi  6949  pmsspw  6969  brdomi  7039  en1uniel  7097  mapdom1g  7153  dif1en  7189  enomnilem  7484  omnimkv  7502  mkvprop  7504  fodjumkvlemres  7505  enmkvlem  7507  enwomnilem  7515  ltrnqi  7794  peano2nnnn  8226  peano2nn  9325  eliooord  10346  fzrev3i  10511  elfzole1  10579  elfzolt2  10580  bcp1nk  11221  rere  11651  climcl  12072  climcau  12137  fprodcnv  12416  isstruct2im  13419  restsspw  13661  mgmcl  13737  submss  13841  subm0cl  13843  submcl  13844  submmnd  13845  subgsubm  14057  ringidval  14371  opprnzr  14601  opprdomn  14692  zrhval  15060  istopfin  15243  uniopn  15244  iunopn  15245  inopn  15246  eltpsg  15283  basis1  15290  basis2  15291  eltg4i  15298  lmff  15492  psmetf  15568  psmet0  15570  psmettri2  15571  metflem  15592  xmetf  15593  xmeteq0  15602  xmettri2  15604  cncff  15820  cncfi  15821  limcresi  15909  dvcnp2cntop  15942  sinq34lt0t  16075  lgsdir2lem2  16370  2sqlem9  16465  edgval  16523  uhgrfm  16536  ushgrfm  16537  upgrfen  16560  umgrfen  16570  uspgrfen  16622  usgrfen  16623  wlkcprim  16813  trlsv  16847  isclwwlkni  16870  eupthv  16909