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  965  ax11i  1702  equsex  1716  eleq1a  2238  ceqsalg  2754  cgsexg  2761  cgsex2g  2762  cgsex4g  2763  ceqsex  2764  spc2egv  2816  spc3egv  2818  csbiebt  3084  dfiin2g  3899  sotricim  4301  ralxfrALT  4445  iunpw  4458  opelxp  4634  ssrel  4692  ssrel2  4694  ssrelrel  4704  iss  4930  funcnvuni  5257  fun11iun  5453  tfrlem8  6286  eroveu  6592  fundmen  6772  nneneq  6823  fidifsnen  6836  prarloclem5  7441  prarloc  7444  recexprlemss1l  7576  recexprlemss1u  7577  uzin  9498  indstr  9531  elfzmlbp  10067