Theorem biimprcd 160

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 157	1 |- ( ch -> ( 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  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimparc  299  pm5.32  453  oplem1  975  ax11i  1714  equsex  1728  eleq1a  2249  ceqsalg  2765  cgsexg  2772  cgsex2g  2773  cgsex4g  2774  ceqsex  2775  spc2egv  2827  spc3egv  2829  csbiebt  3096  dfiin2g  3918  sotricim  4321  ralxfrALT  4465  iunpw  4478  opelxp  4654  ssrel  4712  ssrel2  4714  ssrelrel  4724  iss  4950  funcnvuni  5282  fun11iun  5479  tfrlem8  6314  eroveu  6621  fundmen  6801  nneneq  6852  fidifsnen  6865  prarloclem5  7494  prarloc  7497  recexprlemss1l  7629  recexprlemss1u  7630  uzin  9554  indstr  9587  elfzmlbp  10125