Theorem ibi 175

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 143	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 49	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ibir  176  pm5.21nii  693  elab3gf  2834  elpwi  3519  elsni  3545  elpr2  3549  elpri  3550  eltpi  3570  snssi  3664  prssi  3678  eloni  4297  limuni2  4319  elxpi  4555  releldmb  4776  relelrnb  4777  elrnmpt2d  4794  funeu  5148  fneu  5227  fvelima  5473  eloprabi  6094  fo2ndf  6124  tfrlem9  6216  ecexr  6434  elqsi  6481  qsel  6506  ecopovsym  6525  ecopovsymg  6528  elpmi  6561  elmapi  6564  pmsspw  6577  brdomi  6643  en1uniel  6698  mapdom1g  6741  dif1en  6773  enomnilem  7010  omnimkv  7030  mkvprop  7032  fodjumkvlemres  7033  ltrnqi  7229  peano2nnnn  7661  peano2nn  8732  eliooord  9711  fzrev3i  9868  elfzole1  9932  elfzolt2  9933  bcp1nk  10508  rere  10637  climcl  11051  climcau  11116  isstruct2im  11969  restsspw  12130  istopfin  12167  uniopn  12168  iunopn  12169  inopn  12170  eltpsg  12207  basis1  12214  basis2  12215  eltg4i  12224  lmff  12418  psmetf  12494  psmet0  12496  psmettri2  12497  metflem  12518  xmetf  12519  xmeteq0  12528  xmettri2  12530  cncff  12733  cncfi  12734  limcresi  12804  dvcnp2cntop  12832  sinq34lt0t  12912