Theorem biimprcd 159

Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypothesis

Ref	Expression
biimpcd.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimprcd	|- ( ch -> ( ph -> ps ) )

Proof of Theorem biimprcd

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ch -> ch )
2		biimpcd.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5ibrcom 156	1 |- ( ch -> ( ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimparc  294  pm5.32  442  oplem1  922  ax11i  1650  equsex  1664  eleq1a  2160  ceqsalg  2648  cgsexg  2655  cgsex2g  2656  cgsex4g  2657  ceqsex  2658  spc2egv  2709  spc3egv  2711  csbiebt  2968  dfiin2g  3769  sotricim  4159  ralxfrALT  4302  iunpw  4315  opelxp  4480  ssrel  4539  ssrel2  4541  ssrelrel  4551  iss  4771  funcnvuni  5096  fun11iun  5287  tfrlem8  6097  eroveu  6397  fundmen  6577  nneneq  6627  fidifsnen  6640  prarloclem5  7113  prarloc  7116  recexprlemss1l  7248  recexprlemss1u  7249  uzin  9105  indstr  9135  elfzmlbp  9597