Theorem ibi 449

Description: Inference that converts a biconditional implied by one of its arguments, into an implication.

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 135	. 2 |- (ph -> (ph -> ps))
3	2	pm2.43i 58	1 |- (ph -> ps)

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  ibir 450  elimh 571  elab3g 1420  npss0 1731  elimhyp 1790  elimhyp2v 1791  elimhyp3v 1792  elpw2g 1803  elsni 1827  snssi 1851  eloni 2209  nnlim 2385  abrexex 2912  ecopoprsym 3246  ominf 3423  unblem2 3432  unfilem1 3438  elom3 3478  scott0 3542  indpi 3828  pjch1t 5560  pjv 5589  pjclem4a 5652  pj3lem1 5658  strlem4 5695

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org