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	|- ( ph -> ( ph <-> ps ) )

Assertion

Ref	Expression
ibi	|- ( ph -> ps )

Proof of Theorem ibi

Step	Hyp	Ref	Expression
1		ibi.1	. . 3 |- ( ph -> ( ph <-> ps ) )
2	1	biimpd 144	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 49	1 |- ( ph -> ps )

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  11392  climcl  11809  climcau  11874  fprodcnv  12152  isstruct2im  13058  restsspw  13298  mgmcl  13408  submss  13525  subm0cl  13527  submcl  13528  submmnd  13529  subgsubm  13749  opprnzr  14166  opprdomn  14255  zrhval  14597  istopfin  14690  uniopn  14691  iunopn  14692  inopn  14693  eltpsg  14730  basis1  14737  basis2  14738  eltg4i  14745  lmff  14939  psmetf  15015  psmet0  15017  psmettri2  15018  metflem  15039  xmetf  15040  xmeteq0  15049  xmettri2  15051  cncff  15267  cncfi  15268  limcresi  15356  dvcnp2cntop  15389  sinq34lt0t  15521  lgsdir2lem2  15724  2sqlem9  15819  uhgrfm  15889  ushgrfm  15890  upgrfen  15913  umgrfen  15923  uspgrfen  15973  usgrfen  15974  wlkcprim  16096  trlsv  16128  isclwwlkni  16150