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  6594  ecexr  6816  elqsi  6865  qsel  6890  ecopovsym  6909  ecopovsymg  6912  elpmi  6945  elmapi  6948  pmsspw  6968  brdomi  7037  en1uniel  7095  mapdom1g  7151  dif1en  7187  enomnilem  7484  omnimkv  7502  mkvprop  7504  fodjumkvlemres  7505  enmkvlem  7507  enwomnilem  7515  ltrnqi  7794  peano2nnnn  8226  peano2nn  9325  eliooord  10347  fzrev3i  10512  elfzole1  10580  elfzolt2  10581  bcp1nk  11222  rere  11652  climcl  12073  climcau  12138  fprodcnv  12417  isstruct2im  13420  restsspw  13662  mgmcl  13738  submss  13842  subm0cl  13844  submcl  13845  submmnd  13846  subgsubm  14058  ringidval  14372  opprnzr  14602  opprdomn  14693  zrhval  15061  istopfin  15226  uniopn  15227  iunopn  15228  inopn  15229  eltpsg  15266  basis1  15273  basis2  15274  eltg4i  15281  lmff  15475  psmetf  15551  psmet0  15553  psmettri2  15554  metflem  15575  xmetf  15576  xmeteq0  15585  xmettri2  15587  cncff  15803  cncfi  15804  limcresi  15892  dvcnp2cntop  15925  sinq34lt0t  16058  lgsdir2lem2  16353  2sqlem9  16448  edgval  16506  uhgrfm  16519  ushgrfm  16520  upgrfen  16543  umgrfen  16553  uspgrfen  16605  usgrfen  16606  wlkcprim  16796  trlsv  16830  isclwwlkni  16853  eupthv  16892