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  6361  fo2ndf  6392  elmpom  6403  tfrlem9  6485  ecexr  6707  elqsi  6756  qsel  6781  ecopovsym  6800  ecopovsymg  6803  elpmi  6836  elmapi  6839  pmsspw  6852  brdomi  6920  en1uniel  6978  mapdom1g  7033  dif1en  7068  enomnilem  7337  omnimkv  7355  mkvprop  7357  fodjumkvlemres  7358  enmkvlem  7360  enwomnilem  7368  ltrnqi  7641  peano2nnnn  8073  peano2nn  9155  eliooord  10163  fzrev3i  10323  elfzole1  10391  elfzolt2  10392  bcp1nk  11025  rere  11443  climcl  11860  climcau  11925  fprodcnv  12204  isstruct2im  13110  restsspw  13350  mgmcl  13460  submss  13577  subm0cl  13579  submcl  13580  submmnd  13581  subgsubm  13801  opprnzr  14219  opprdomn  14308  zrhval  14650  istopfin  14743  uniopn  14744  iunopn  14745  inopn  14746  eltpsg  14783  basis1  14790  basis2  14791  eltg4i  14798  lmff  14992  psmetf  15068  psmet0  15070  psmettri2  15071  metflem  15092  xmetf  15093  xmeteq0  15102  xmettri2  15104  cncff  15320  cncfi  15321  limcresi  15409  dvcnp2cntop  15442  sinq34lt0t  15574  lgsdir2lem2  15777  2sqlem9  15872  edgval  15930  uhgrfm  15943  ushgrfm  15944  upgrfen  15967  umgrfen  15977  uspgrfen  16029  usgrfen  16030  wlkcprim  16220  trlsv  16254  isclwwlkni  16277  eupthv  16316