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  3615  elsni  3641  elpr2  3645  elpri  3646  eltpi  3670  snssi  3767  prssi  3781  eloni  4411  limuni2  4433  elxpi  4680  releldmb  4904  relelrnb  4905  elrnmpt2d  4922  elrelimasn  5036  funeu  5284  fneu  5363  fvelima  5613  eloprabi  6256  fo2ndf  6287  tfrlem9  6379  ecexr  6599  elqsi  6648  qsel  6673  ecopovsym  6692  ecopovsymg  6695  elpmi  6728  elmapi  6731  pmsspw  6744  brdomi  6810  en1uniel  6865  mapdom1g  6910  dif1en  6942  enomnilem  7206  omnimkv  7224  mkvprop  7226  fodjumkvlemres  7227  enmkvlem  7229  enwomnilem  7237  ltrnqi  7491  peano2nnnn  7923  peano2nn  9005  eliooord  10006  fzrev3i  10166  elfzole1  10234  elfzolt2  10235  bcp1nk  10857  rere  11033  climcl  11450  climcau  11515  fprodcnv  11793  isstruct2im  12699  restsspw  12937  mgmcl  13028  submss  13134  subm0cl  13136  submcl  13137  submmnd  13138  subgsubm  13352  opprnzr  13768  opprdomn  13857  zrhval  14199  istopfin  14262  uniopn  14263  iunopn  14264  inopn  14265  eltpsg  14302  basis1  14309  basis2  14310  eltg4i  14317  lmff  14511  psmetf  14587  psmet0  14589  psmettri2  14590  metflem  14611  xmetf  14612  xmeteq0  14621  xmettri2  14623  cncff  14839  cncfi  14840  limcresi  14928  dvcnp2cntop  14961  sinq34lt0t  15093  lgsdir2lem2  15296  2sqlem9  15391