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  712  elab3gf  2970  elpwi  3683  elsni  3712  elpr2  3716  elpri  3717  eltpi  3741  snssi  3843  prssi  3857  eloni  4501  limuni2  4523  elxpi  4770  releldmb  4999  relelrnb  5000  elrnmpt2d  5017  elrelimasn  5133  funeu  5382  fneu  5467  fvelima  5733  eloprabi  6405  fo2ndf  6436  elmpom  6447  fczsupp0  6472  tfrlem9  6563  ecexr  6785  elqsi  6834  qsel  6859  ecopovsym  6878  ecopovsymg  6881  elpmi  6914  elmapi  6917  pmsspw  6930  brdomi  6999  en1uniel  7057  mapdom1g  7113  dif1en  7149  enomnilem  7442  omnimkv  7460  mkvprop  7462  fodjumkvlemres  7463  enmkvlem  7465  enwomnilem  7473  ltrnqi  7752  peano2nnnn  8184  peano2nn  9266  eliooord  10280  fzrev3i  10444  elfzole1  10512  elfzolt2  10513  bcp1nk  11149  rere  11575  climcl  11992  climcau  12057  fprodcnv  12336  isstruct2im  13306  restsspw  13546  mgmcl  13622  submss  13731  subm0cl  13733  submcl  13734  submmnd  13735  subgsubm  13949  opprnzr  14431  opprdomn  14522  zrhval  14891  istopfin  14991  uniopn  14992  iunopn  14993  inopn  14994  eltpsg  15031  basis1  15038  basis2  15039  eltg4i  15046  lmff  15240  psmetf  15316  psmet0  15318  psmettri2  15319  metflem  15340  xmetf  15341  xmeteq0  15350  xmettri2  15352  cncff  15568  cncfi  15569  limcresi  15657  dvcnp2cntop  15690  sinq34lt0t  15822  lgsdir2lem2  16028  2sqlem9  16123  edgval  16181  uhgrfm  16194  ushgrfm  16195  upgrfen  16218  umgrfen  16228  uspgrfen  16280  usgrfen  16281  wlkcprim  16471  trlsv  16505  isclwwlkni  16528  eupthv  16567