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  5685  eloprabi  6342  fo2ndf  6373  tfrlem9  6465  ecexr  6685  elqsi  6734  qsel  6759  ecopovsym  6778  ecopovsymg  6781  elpmi  6814  elmapi  6817  pmsspw  6830  brdomi  6898  en1uniel  6956  mapdom1g  7008  dif1en  7041  enomnilem  7305  omnimkv  7323  mkvprop  7325  fodjumkvlemres  7326  enmkvlem  7328  enwomnilem  7336  ltrnqi  7608  peano2nnnn  8040  peano2nn  9122  eliooord  10124  fzrev3i  10284  elfzole1  10352  elfzolt2  10353  bcp1nk  10984  rere  11376  climcl  11793  climcau  11858  fprodcnv  12136  isstruct2im  13042  restsspw  13282  mgmcl  13392  submss  13509  subm0cl  13511  submcl  13512  submmnd  13513  subgsubm  13733  opprnzr  14150  opprdomn  14239  zrhval  14581  istopfin  14674  uniopn  14675  iunopn  14676  inopn  14677  eltpsg  14714  basis1  14721  basis2  14722  eltg4i  14729  lmff  14923  psmetf  14999  psmet0  15001  psmettri2  15002  metflem  15023  xmetf  15024  xmeteq0  15033  xmettri2  15035  cncff  15251  cncfi  15252  limcresi  15340  dvcnp2cntop  15373  sinq34lt0t  15505  lgsdir2lem2  15708  2sqlem9  15803  uhgrfm  15873  ushgrfm  15874  upgrfen  15897  umgrfen  15907  uspgrfen  15957  usgrfen  15958  wlkcprim  16061