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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimparc  297  pm5.32  449  oplem1  960  ax11i  1694  equsex  1708  eleq1a  2229  ceqsalg  2740  cgsexg  2747  cgsex2g  2748  cgsex4g  2749  ceqsex  2750  spc2egv  2802  spc3egv  2804  csbiebt  3070  dfiin2g  3882  sotricim  4282  ralxfrALT  4425  iunpw  4438  opelxp  4613  ssrel  4671  ssrel2  4673  ssrelrel  4683  iss  4909  funcnvuni  5236  fun11iun  5432  tfrlem8  6259  eroveu  6564  fundmen  6744  nneneq  6795  fidifsnen  6808  prarloclem5  7403  prarloc  7406  recexprlemss1l  7538  recexprlemss1u  7539  uzin  9454  indstr  9487  elfzmlbp  10013