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  712  elab3gf  2967  elpwi  3678  elsni  3707  elpr2  3711  elpri  3712  eltpi  3736  snssi  3838  prssi  3852  eloni  4496  limuni2  4518  elxpi  4765  releldmb  4994  relelrnb  4995  elrnmpt2d  5012  elrelimasn  5128  funeu  5377  fneu  5462  fvelima  5728  eloprabi  6392  fo2ndf  6423  elmpom  6434  fczsupp0  6459  tfrlem9  6550  ecexr  6772  elqsi  6821  qsel  6846  ecopovsym  6865  ecopovsymg  6868  elpmi  6901  elmapi  6904  pmsspw  6917  brdomi  6986  en1uniel  7044  mapdom1g  7100  dif1en  7136  enomnilem  7429  omnimkv  7447  mkvprop  7449  fodjumkvlemres  7450  enmkvlem  7452  enwomnilem  7460  ltrnqi  7736  peano2nnnn  8168  peano2nn  9249  eliooord  10261  fzrev3i  10422  elfzole1  10490  elfzolt2  10491  bcp1nk  11124  rere  11550  climcl  11967  climcau  12032  fprodcnv  12311  isstruct2im  13222  restsspw  13462  mgmcl  13572  submss  13689  subm0cl  13691  submcl  13692  submmnd  13693  subgsubm  13913  opprnzr  14331  opprdomn  14421  zrhval  14765  istopfin  14865  uniopn  14866  iunopn  14867  inopn  14868  eltpsg  14905  basis1  14912  basis2  14913  eltg4i  14920  lmff  15114  psmetf  15190  psmet0  15192  psmettri2  15193  metflem  15214  xmetf  15215  xmeteq0  15224  xmettri2  15226  cncff  15442  cncfi  15443  limcresi  15531  dvcnp2cntop  15564  sinq34lt0t  15696  lgsdir2lem2  15902  2sqlem9  15997  edgval  16055  uhgrfm  16068  ushgrfm  16069  upgrfen  16092  umgrfen  16102  uspgrfen  16154  usgrfen  16155  wlkcprim  16345  trlsv  16379  isclwwlkni  16402  eupthv  16441