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  705  elab3gf  2914  elpwi  3614  elsni  3640  elpr2  3644  elpri  3645  eltpi  3669  snssi  3766  prssi  3780  eloni  4410  limuni2  4432  elxpi  4679  releldmb  4903  relelrnb  4904  elrnmpt2d  4921  elrelimasn  5035  funeu  5283  fneu  5362  fvelima  5612  eloprabi  6254  fo2ndf  6285  tfrlem9  6377  ecexr  6597  elqsi  6646  qsel  6671  ecopovsym  6690  ecopovsymg  6693  elpmi  6726  elmapi  6729  pmsspw  6742  brdomi  6808  en1uniel  6863  mapdom1g  6908  dif1en  6940  enomnilem  7204  omnimkv  7222  mkvprop  7224  fodjumkvlemres  7225  enmkvlem  7227  enwomnilem  7235  ltrnqi  7488  peano2nnnn  7920  peano2nn  9002  eliooord  10003  fzrev3i  10163  elfzole1  10231  elfzolt2  10232  bcp1nk  10854  rere  11030  climcl  11447  climcau  11512  fprodcnv  11790  isstruct2im  12688  restsspw  12920  mgmcl  13002  submss  13108  subm0cl  13110  submcl  13111  submmnd  13112  subgsubm  13326  opprnzr  13742  opprdomn  13831  zrhval  14173  istopfin  14236  uniopn  14237  iunopn  14238  inopn  14239  eltpsg  14276  basis1  14283  basis2  14284  eltg4i  14291  lmff  14485  psmetf  14561  psmet0  14563  psmettri2  14564  metflem  14585  xmetf  14586  xmeteq0  14595  xmettri2  14597  cncff  14813  cncfi  14814  limcresi  14902  dvcnp2cntop  14935  sinq34lt0t  15067  lgsdir2lem2  15270  2sqlem9  15365