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  716  elab3gf  2976  elpwi  3694  elsni  3723  elpr2  3727  elpri  3728  eltpi  3752  snssi  3854  prssi  3868  eloni  4515  limuni2  4537  elxpi  4785  releldmb  5014  relelrnb  5015  elrnmpt2d  5032  elrelimasn  5148  funeu  5397  fneu  5482  fvelima  5748  eloprabi  6422  fo2ndf  6453  elmpom  6464  fczsupp0  6489  tfrlem9  6580  ecexr  6802  elqsi  6851  qsel  6876  ecopovsym  6895  ecopovsymg  6898  elpmi  6931  elmapi  6934  pmsspw  6954  brdomi  7023  en1uniel  7081  mapdom1g  7137  dif1en  7173  enomnilem  7468  omnimkv  7486  mkvprop  7488  fodjumkvlemres  7489  enmkvlem  7491  enwomnilem  7499  ltrnqi  7778  peano2nnnn  8210  peano2nn  9295  eliooord  10309  fzrev3i  10473  elfzole1  10541  elfzolt2  10542  bcp1nk  11178  rere  11608  climcl  12026  climcau  12091  fprodcnv  12370  isstruct2im  13340  restsspw  13580  mgmcl  13656  submss  13760  subm0cl  13762  submcl  13763  submmnd  13764  subgsubm  13976  opprnzr  14466  opprdomn  14557  zrhval  14924  istopfin  15024  uniopn  15025  iunopn  15026  inopn  15027  eltpsg  15064  basis1  15071  basis2  15072  eltg4i  15079  lmff  15273  psmetf  15349  psmet0  15351  psmettri2  15352  metflem  15373  xmetf  15374  xmeteq0  15383  xmettri2  15385  cncff  15601  cncfi  15602  limcresi  15690  dvcnp2cntop  15723  sinq34lt0t  15855  lgsdir2lem2  16062  2sqlem9  16157  edgval  16215  uhgrfm  16228  ushgrfm  16229  upgrfen  16252  umgrfen  16262  uspgrfen  16314  usgrfen  16315  wlkcprim  16505  trlsv  16539  isclwwlkni  16562  eupthv  16601