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  705  elab3gf  2911  elpwi  3611  elsni  3637  elpr2  3641  elpri  3642  eltpi  3666  snssi  3763  prssi  3777  eloni  4407  limuni2  4429  elxpi  4676  releldmb  4900  relelrnb  4901  elrnmpt2d  4918  elrelimasn  5032  funeu  5280  fneu  5359  fvelima  5609  eloprabi  6251  fo2ndf  6282  tfrlem9  6374  ecexr  6594  elqsi  6643  qsel  6668  ecopovsym  6687  ecopovsymg  6690  elpmi  6723  elmapi  6726  pmsspw  6739  brdomi  6805  en1uniel  6860  mapdom1g  6905  dif1en  6937  enomnilem  7199  omnimkv  7217  mkvprop  7219  fodjumkvlemres  7220  enmkvlem  7222  enwomnilem  7230  ltrnqi  7483  peano2nnnn  7915  peano2nn  8996  eliooord  9997  fzrev3i  10157  elfzole1  10225  elfzolt2  10226  bcp1nk  10836  rere  11012  climcl  11428  climcau  11493  fprodcnv  11771  isstruct2im  12631  restsspw  12863  mgmcl  12945  submss  13051  subm0cl  13053  submcl  13054  submmnd  13055  subgsubm  13269  opprnzr  13685  opprdomn  13774  zrhval  14116  istopfin  14179  uniopn  14180  iunopn  14181  inopn  14182  eltpsg  14219  basis1  14226  basis2  14227  eltg4i  14234  lmff  14428  psmetf  14504  psmet0  14506  psmettri2  14507  metflem  14528  xmetf  14529  xmeteq0  14538  xmettri2  14540  cncff  14756  cncfi  14757  limcresi  14845  dvcnp2cntop  14878  sinq34lt0t  15007  lgsdir2lem2  15186  2sqlem9  15281