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  2914  elpwi  3615  elsni  3641  elpr2  3645  elpri  3646  eltpi  3670  snssi  3767  prssi  3781  eloni  4411  limuni2  4433  elxpi  4680  releldmb  4904  relelrnb  4905  elrnmpt2d  4922  elrelimasn  5036  funeu  5284  fneu  5365  fvelima  5615  eloprabi  6263  fo2ndf  6294  tfrlem9  6386  ecexr  6606  elqsi  6655  qsel  6680  ecopovsym  6699  ecopovsymg  6702  elpmi  6735  elmapi  6738  pmsspw  6751  brdomi  6817  en1uniel  6872  mapdom1g  6917  dif1en  6949  enomnilem  7213  omnimkv  7231  mkvprop  7233  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  ltrnqi  7505  peano2nnnn  7937  peano2nn  9019  eliooord  10020  fzrev3i  10180  elfzole1  10248  elfzolt2  10249  bcp1nk  10871  rere  11047  climcl  11464  climcau  11529  fprodcnv  11807  isstruct2im  12713  restsspw  12951  mgmcl  13061  submss  13178  subm0cl  13180  submcl  13181  submmnd  13182  subgsubm  13402  opprnzr  13818  opprdomn  13907  zrhval  14249  istopfin  14320  uniopn  14321  iunopn  14322  inopn  14323  eltpsg  14360  basis1  14367  basis2  14368  eltg4i  14375  lmff  14569  psmetf  14645  psmet0  14647  psmettri2  14648  metflem  14669  xmetf  14670  xmeteq0  14679  xmettri2  14681  cncff  14897  cncfi  14898  limcresi  14986  dvcnp2cntop  15019  sinq34lt0t  15151  lgsdir2lem2  15354  2sqlem9  15449