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  2957  elpwi  3665  elsni  3691  elpr2  3695  elpri  3696  eltpi  3720  snssi  3822  prssi  3836  eloni  4478  limuni2  4500  elxpi  4747  releldmb  4975  relelrnb  4976  elrnmpt2d  4993  elrelimasn  5109  funeu  5358  fneu  5443  fvelima  5706  eloprabi  6370  fo2ndf  6401  elmpom  6412  fczsupp0  6437  tfrlem9  6528  ecexr  6750  elqsi  6799  qsel  6824  ecopovsym  6843  ecopovsymg  6846  elpmi  6879  elmapi  6882  pmsspw  6895  brdomi  6963  en1uniel  7021  mapdom1g  7076  dif1en  7111  enomnilem  7397  omnimkv  7415  mkvprop  7417  fodjumkvlemres  7418  enmkvlem  7420  enwomnilem  7428  ltrnqi  7701  peano2nnnn  8133  peano2nn  9214  eliooord  10224  fzrev3i  10385  elfzole1  10453  elfzolt2  10454  bcp1nk  11087  rere  11505  climcl  11922  climcau  11987  fprodcnv  12266  isstruct2im  13172  restsspw  13412  mgmcl  13522  submss  13639  subm0cl  13641  submcl  13642  submmnd  13643  subgsubm  13863  opprnzr  14281  opprdomn  14371  zrhval  14713  istopfin  14811  uniopn  14812  iunopn  14813  inopn  14814  eltpsg  14851  basis1  14858  basis2  14859  eltg4i  14866  lmff  15060  psmetf  15136  psmet0  15138  psmettri2  15139  metflem  15160  xmetf  15161  xmeteq0  15170  xmettri2  15172  cncff  15388  cncfi  15389  limcresi  15477  dvcnp2cntop  15510  sinq34lt0t  15642  lgsdir2lem2  15848  2sqlem9  15943  edgval  16001  uhgrfm  16014  ushgrfm  16015  upgrfen  16038  umgrfen  16048  uspgrfen  16100  usgrfen  16101  wlkcprim  16291  trlsv  16325  isclwwlkni  16348  eupthv  16387