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  706  elab3gf  2930  elpwi  3635  elsni  3661  elpr2  3665  elpri  3666  eltpi  3690  snssi  3788  prssi  3802  eloni  4440  limuni2  4462  elxpi  4709  releldmb  4934  relelrnb  4935  elrnmpt2d  4952  elrelimasn  5067  funeu  5315  fneu  5399  fvelima  5653  eloprabi  6305  fo2ndf  6336  tfrlem9  6428  ecexr  6648  elqsi  6697  qsel  6722  ecopovsym  6741  ecopovsymg  6744  elpmi  6777  elmapi  6780  pmsspw  6793  brdomi  6861  en1uniel  6919  mapdom1g  6969  dif1en  7002  enomnilem  7266  omnimkv  7284  mkvprop  7286  fodjumkvlemres  7287  enmkvlem  7289  enwomnilem  7297  ltrnqi  7569  peano2nnnn  8001  peano2nn  9083  eliooord  10085  fzrev3i  10245  elfzole1  10313  elfzolt2  10314  bcp1nk  10944  rere  11291  climcl  11708  climcau  11773  fprodcnv  12051  isstruct2im  12957  restsspw  13196  mgmcl  13306  submss  13423  subm0cl  13425  submcl  13426  submmnd  13427  subgsubm  13647  opprnzr  14063  opprdomn  14152  zrhval  14494  istopfin  14587  uniopn  14588  iunopn  14589  inopn  14590  eltpsg  14627  basis1  14634  basis2  14635  eltg4i  14642  lmff  14836  psmetf  14912  psmet0  14914  psmettri2  14915  metflem  14936  xmetf  14937  xmeteq0  14946  xmettri2  14948  cncff  15164  cncfi  15165  limcresi  15253  dvcnp2cntop  15286  sinq34lt0t  15418  lgsdir2lem2  15621  2sqlem9  15716  uhgrfm  15784  ushgrfm  15785  upgrfen  15808  umgrfen  15818