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  704  elab3gf  2888  elpwi  3585  elsni  3611  elpr2  3615  elpri  3616  eltpi  3640  snssi  3737  prssi  3751  eloni  4376  limuni2  4398  elxpi  4643  releldmb  4865  relelrnb  4866  elrnmpt2d  4883  elrelimasn  4995  funeu  5242  fneu  5321  fvelima  5568  eloprabi  6197  fo2ndf  6228  tfrlem9  6320  ecexr  6540  elqsi  6587  qsel  6612  ecopovsym  6631  ecopovsymg  6634  elpmi  6667  elmapi  6670  pmsspw  6683  brdomi  6749  en1uniel  6804  mapdom1g  6847  dif1en  6879  enomnilem  7136  omnimkv  7154  mkvprop  7156  fodjumkvlemres  7157  enmkvlem  7159  enwomnilem  7167  ltrnqi  7420  peano2nnnn  7852  peano2nn  8931  eliooord  9928  fzrev3i  10088  elfzole1  10155  elfzolt2  10156  bcp1nk  10742  rere  10874  climcl  11290  climcau  11355  fprodcnv  11633  isstruct2im  12472  restsspw  12698  mgmcl  12778  submss  12867  subm0cl  12869  submcl  12870  subgsubm  13056  istopfin  13503  uniopn  13504  iunopn  13505  inopn  13506  eltpsg  13543  basis1  13550  basis2  13551  eltg4i  13558  lmff  13752  psmetf  13828  psmet0  13830  psmettri2  13831  metflem  13852  xmetf  13853  xmeteq0  13862  xmettri2  13864  cncff  14067  cncfi  14068  limcresi  14138  dvcnp2cntop  14166  sinq34lt0t  14255  lgsdir2lem2  14433  2sqlem9  14474