Theorem ibi 175

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 143	. 2 |- ( ph -> ( ph -> ps ) )
3	2	pm2.43i 49	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ibir  176  pm5.21nii  699  elab3gf  2880  elpwi  3573  elsni  3599  elpr2  3603  elpri  3604  eltpi  3628  snssi  3722  prssi  3736  eloni  4358  limuni2  4380  elxpi  4625  releldmb  4846  relelrnb  4847  elrnmpt2d  4864  funeu  5221  fneu  5300  fvelima  5546  eloprabi  6172  fo2ndf  6203  tfrlem9  6295  ecexr  6514  elqsi  6561  qsel  6586  ecopovsym  6605  ecopovsymg  6608  elpmi  6641  elmapi  6644  pmsspw  6657  brdomi  6723  en1uniel  6778  mapdom1g  6821  dif1en  6853  enomnilem  7110  omnimkv  7128  mkvprop  7130  fodjumkvlemres  7131  enmkvlem  7133  enwomnilem  7141  ltrnqi  7370  peano2nnnn  7802  peano2nn  8877  eliooord  9872  fzrev3i  10031  elfzole1  10098  elfzolt2  10099  bcp1nk  10683  rere  10816  climcl  11232  climcau  11297  fprodcnv  11575  isstruct2im  12413  restsspw  12576  mgmcl  12600  submss  12685  subm0cl  12687  submcl  12688  istopfin  12751  uniopn  12752  iunopn  12753  inopn  12754  eltpsg  12791  basis1  12798  basis2  12799  eltg4i  12808  lmff  13002  psmetf  13078  psmet0  13080  psmettri2  13081  metflem  13102  xmetf  13103  xmeteq0  13112  xmettri2  13114  cncff  13317  cncfi  13318  limcresi  13388  dvcnp2cntop  13416  sinq34lt0t  13505  lgsdir2lem2  13683  2sqlem9  13713