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  711  elab3gf  2956  elpwi  3661  elsni  3687  elpr2  3691  elpri  3692  eltpi  3716  snssi  3817  prssi  3831  eloni  4472  limuni2  4494  elxpi  4741  releldmb  4969  relelrnb  4970  elrnmpt2d  4987  elrelimasn  5102  funeu  5351  fneu  5436  fvelima  5697  eloprabi  6360  fo2ndf  6391  elmpom  6402  tfrlem9  6484  ecexr  6706  elqsi  6755  qsel  6780  ecopovsym  6799  ecopovsymg  6802  elpmi  6835  elmapi  6838  pmsspw  6851  brdomi  6919  en1uniel  6977  mapdom1g  7032  dif1en  7067  enomnilem  7336  omnimkv  7354  mkvprop  7356  fodjumkvlemres  7357  enmkvlem  7359  enwomnilem  7367  ltrnqi  7640  peano2nnnn  8072  peano2nn  9154  eliooord  10162  fzrev3i  10322  elfzole1  10390  elfzolt2  10391  bcp1nk  11023  rere  11425  climcl  11842  climcau  11907  fprodcnv  12185  isstruct2im  13091  restsspw  13331  mgmcl  13441  submss  13558  subm0cl  13560  submcl  13561  submmnd  13562  subgsubm  13782  opprnzr  14199  opprdomn  14288  zrhval  14630  istopfin  14723  uniopn  14724  iunopn  14725  inopn  14726  eltpsg  14763  basis1  14770  basis2  14771  eltg4i  14778  lmff  14972  psmetf  15048  psmet0  15050  psmettri2  15051  metflem  15072  xmetf  15073  xmeteq0  15082  xmettri2  15084  cncff  15300  cncfi  15301  limcresi  15389  dvcnp2cntop  15422  sinq34lt0t  15554  lgsdir2lem2  15757  2sqlem9  15852  edgval  15910  uhgrfm  15923  ushgrfm  15924  upgrfen  15947  umgrfen  15957  uspgrfen  16009  usgrfen  16010  wlkcprim  16200  trlsv  16234  isclwwlkni  16257  eupthv  16296