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  2910  elpwi  3610  elsni  3636  elpr2  3640  elpri  3641  eltpi  3665  snssi  3762  prssi  3776  eloni  4406  limuni2  4428  elxpi  4675  releldmb  4899  relelrnb  4900  elrnmpt2d  4917  elrelimasn  5031  funeu  5279  fneu  5358  fvelima  5608  eloprabi  6249  fo2ndf  6280  tfrlem9  6372  ecexr  6592  elqsi  6641  qsel  6666  ecopovsym  6685  ecopovsymg  6688  elpmi  6721  elmapi  6724  pmsspw  6737  brdomi  6803  en1uniel  6858  mapdom1g  6903  dif1en  6935  enomnilem  7197  omnimkv  7215  mkvprop  7217  fodjumkvlemres  7218  enmkvlem  7220  enwomnilem  7228  ltrnqi  7481  peano2nnnn  7913  peano2nn  8994  eliooord  9994  fzrev3i  10154  elfzole1  10222  elfzolt2  10223  bcp1nk  10833  rere  11009  climcl  11425  climcau  11490  fprodcnv  11768  isstruct2im  12628  restsspw  12860  mgmcl  12942  submss  13048  subm0cl  13050  submcl  13051  submmnd  13052  subgsubm  13266  opprnzr  13682  opprdomn  13771  zrhval  14105  istopfin  14168  uniopn  14169  iunopn  14170  inopn  14171  eltpsg  14208  basis1  14215  basis2  14216  eltg4i  14223  lmff  14417  psmetf  14493  psmet0  14495  psmettri2  14496  metflem  14517  xmetf  14518  xmeteq0  14527  xmettri2  14529  cncff  14732  cncfi  14733  limcresi  14820  dvcnp2cntop  14848  sinq34lt0t  14966  lgsdir2lem2  15145  2sqlem9  15211