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  709  elab3gf  2953  elpwi  3658  elsni  3684  elpr2  3688  elpri  3689  eltpi  3713  snssi  3812  prssi  3826  eloni  4466  limuni2  4488  elxpi  4735  releldmb  4961  relelrnb  4962  elrnmpt2d  4979  elrelimasn  5094  funeu  5343  fneu  5427  fvelima  5687  eloprabi  6348  fo2ndf  6379  tfrlem9  6471  ecexr  6693  elqsi  6742  qsel  6767  ecopovsym  6786  ecopovsymg  6789  elpmi  6822  elmapi  6825  pmsspw  6838  brdomi  6906  en1uniel  6964  mapdom1g  7016  dif1en  7049  enomnilem  7316  omnimkv  7334  mkvprop  7336  fodjumkvlemres  7337  enmkvlem  7339  enwomnilem  7347  ltrnqi  7619  peano2nnnn  8051  peano2nn  9133  eliooord  10136  fzrev3i  10296  elfzole1  10364  elfzolt2  10365  bcp1nk  10996  rere  11391  climcl  11808  climcau  11873  fprodcnv  12151  isstruct2im  13057  restsspw  13297  mgmcl  13407  submss  13524  subm0cl  13526  submcl  13527  submmnd  13528  subgsubm  13748  opprnzr  14165  opprdomn  14254  zrhval  14596  istopfin  14689  uniopn  14690  iunopn  14691  inopn  14692  eltpsg  14729  basis1  14736  basis2  14737  eltg4i  14744  lmff  14938  psmetf  15014  psmet0  15016  psmettri2  15017  metflem  15038  xmetf  15039  xmeteq0  15048  xmettri2  15050  cncff  15266  cncfi  15267  limcresi  15355  dvcnp2cntop  15388  sinq34lt0t  15520  lgsdir2lem2  15723  2sqlem9  15818  uhgrfm  15888  ushgrfm  15889  upgrfen  15912  umgrfen  15922  uspgrfen  15972  usgrfen  15973  wlkcprim  16091  trlsv  16123