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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  ibir  177  pm5.21nii  716  elab3gf  2976  elpwi  3698  elsni  3727  elpr2  3731  elpri  3732  eltpi  3756  snssi  3859  prssi  3873  eloni  4520  limuni2  4542  elxpi  4790  releldmb  5019  relelrnb  5020  elrnmpt2d  5037  elrelimasn  5153  funeu  5402  fneu  5487  fvelima  5754  eloprabi  6432  fo2ndf  6463  elmpom  6474  fczsupp0  6499  tfrlem9  6590  ecexr  6812  elqsi  6861  qsel  6886  ecopovsym  6905  ecopovsymg  6908  elpmi  6941  elmapi  6944  pmsspw  6964  brdomi  7033  en1uniel  7091  mapdom1g  7147  dif1en  7183  enomnilem  7478  omnimkv  7496  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  enwomnilem  7509  ltrnqi  7788  peano2nnnn  8220  peano2nn  9316  eliooord  10330  fzrev3i  10495  elfzole1  10563  elfzolt2  10564  bcp1nk  11200  rere  11630  climcl  12048  climcau  12113  fprodcnv  12392  isstruct2im  13362  restsspw  13603  mgmcl  13679  submss  13783  subm0cl  13785  submcl  13786  submmnd  13787  subgsubm  13999  ringidval  14265  opprnzr  14493  opprdomn  14584  zrhval  14952  istopfin  15101  uniopn  15102  iunopn  15103  inopn  15104  eltpsg  15141  basis1  15148  basis2  15149  eltg4i  15156  lmff  15350  psmetf  15426  psmet0  15428  psmettri2  15429  metflem  15450  xmetf  15451  xmeteq0  15460  xmettri2  15462  cncff  15678  cncfi  15679  limcresi  15767  dvcnp2cntop  15800  sinq34lt0t  15932  lgsdir2lem2  16148  2sqlem9  16243  edgval  16301  uhgrfm  16314  ushgrfm  16315  upgrfen  16338  umgrfen  16348  uspgrfen  16400  usgrfen  16401  wlkcprim  16591  trlsv  16625  isclwwlkni  16648  eupthv  16687